Theorem AddSubgroup.cyclic_of_min

Modification history

2024-09-10 16:36

Mathlib/GroupTheory/Archimedean.lean

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

Deleted AddSubgroup.cyclic_of_min View on Github →

2023-01-26 16:33

Mathlib/GroupTheory/Archimedean.lean

feat: port GroupTheory.Archimedean (#1856) …

Added AddSubgroup.cyclic_of_min View on Github →