Theorem LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered

Modification history

2024-10-18 15:48
Mathlib/GroupTheory/ArchimedeanDensely.lean
feat(GroupTheory/ArchimedeanDensely): discrete iff not densely ordered (#16618) …
Added LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrderedView on Github →