Commit 2025-08-20 19:33 af5e85d1
View on Github →chore: strengthen denselyOrdered_units_iff (#28688)
Where G₀ is a linearly ordered commutative group with zero, we once had Nontrivial G₀ˣ → (DenselyOrdered G₀ˣ ↔ DenselyOrdered G₀), we now strengthen it to DenselyOrdered G₀ ↔ (Nontrivial G₀ˣ ∧ DenselyOrdered G₀ˣ). We also provide the decreasing instances from this equivalence.