Theorem AddSubgroup.cyclic_of_isolated_zero

Modification history

2024-09-10 16:36

Mathlib/GroupTheory/Archimedean.lean

feat(GroupTheory/Archimedean): multiplicativize to also LinearOrderedCommGroup (#15824)

Deleted AddSubgroup.cyclic_of_isolated_zero View on Github →

2023-03-06 08:38

Mathlib/GroupTheory/Archimedean.lean

feat: port Topology.Instances.Real (#2633) …

Added AddSubgroup.cyclic_of_isolated_zero View on Github →