Theorem CauSeq.Completion.ofRat_injective

Modification history

2025-06-06 01:24
Mathlib/Algebra/Order/CauSeq/Completion.lean
chore: trivial `Nontrivial`ities (#25506) …
Added CauSeq.Completion.ofRat_injectiveView on Github →