Theorem denselyOrdered_units_iff

Modification history

2026-02-15 14:33
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
style: fix many leading by's in mathlib (#35343) …
Modified denselyOrdered_units_iffView on Github →
2025-08-20 19:33
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
chore: strengthen denselyOrdered_units_iff (#28688) …
Modified denselyOrdered_units_iffView on Github →
2024-10-18 15:48
Mathlib/GroupTheory/ArchimedeanDensely.lean
feat(GroupTheory/ArchimedeanDensely): discrete iff not densely ordered (#16618) …
Added denselyOrdered_units_iffView on Github →