Theorem LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_int

Modification history

2025-10-28 21:32
Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
feat(Topology/Algebra/Order/Archimedean): subgroups cyclic iff discrete (#30471) …
Added LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_intView on Github →