Theorem denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units

Modification history

2025-08-20 19:33
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
chore: strengthen denselyOrdered_units_iff (#28688) …
Added denselyOrdered_iff_denselyOrdered_units_and_nontrivial_unitsView on Github →