Commit 2024-09-10 16:36 410eaaab

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Order.lean

deleted theorem abs_mem_iff

added theorem mabs_mem_iff

Modified Mathlib/GroupTheory/Archimedean.lean

deleted theorem AddSubgroup.cyclic_of_isolated_zero

deleted theorem AddSubgroup.cyclic_of_min

deleted theorem AddSubgroup.exists_isLeast_pos

added theorem Subgroup.cyclic_of_isolated_one

added theorem Subgroup.cyclic_of_min

added theorem Subgroup.exists_isLeast_one_lt

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

deleted theorem AddSubgroup.isLeast_closure_iff_eq_abs

modified theorem LinearOrderedAddCommGroup.discrete_or_denselyOrdered

added theorem LinearOrderedCommGroup.discrete_or_denselyOrdered

added theorem Subgroup.isLeast_of_closure_iff_eq_mabs