Commit 2024-09-05 11:40 3e18f177

View on Github →

feat(GroupTheory/ArchimedeanDensely): LinearOrderedAddCommGroup.discrete_or_denselyOrdered (#15659) Classify linearly ordered archimedean additive groups, either they are discrete (order isomorphic to Int) or densely ordered. Also add some simple lemmas about the closure subgroup.

Estimated changes

Modified Mathlib.lean

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

added theorem Subgroup.mem_closure_singleton_self

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

added theorem MulEquiv.strictMono_subsemigroupCongr

added theorem MulEquiv.strictMono_symm

added theorem Subsemigroup.strictMono_topEquiv

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

added theorem Subgroup.closure_singleton_inv

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

added theorem AddSubgroup.closure_singleton_int_one_eq_top

added theorem AddSubgroup.zmultiples_one_eq_top

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

added theorem zpow_right_inj

Created Mathlib/GroupTheory/ArchimedeanDensely.lean

added theorem AddSubgroup.isLeast_closure_iff_eq_abs

added theorem LinearOrderedAddCommGroup.discrete_or_denselyOrdered

added theorem Subgroup.mem_closure_singleton_iff_existsUnique_zpow

Modified Mathlib/Logic/Equiv/Set.lean

added theorem Equiv.Set.Equiv.strictMono_setCongr