Theorem WithZero.denselyOrdered_set_iff_subsingleton

Modification history

2025-07-24 19:33
Mathlib/GroupTheory/ArchimedeanDensely.lean
feat(Order/DenselyOrderedLocallyFinite): linear locally finite dense orders are trivial (#27172)
Added WithZero.denselyOrdered_set_iff_subsingletonView on Github →