Commit 2025-07-29 04:18 9b794ab4

View on Github →

feat(Algebra/Order): Locally Finite Linearly Ordered Abelian Groups (#27430) We prove that ℤ is the only Locally Finite Linearly Ordered Abelian Group. We also move OrderMonoidIso.toAdditive and friends from Mathlib/GroupTheory/ArchimedeanDensely.lean to a new file.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Hom/TypeTags.lean

added def OrderAddMonoidIso.toAdditive_toMultiplicative

added def OrderAddMonoidIso.toMultiplicative''

added def OrderAddMonoidIso.toMultiplicative'

added def OrderAddMonoidIso.toMultiplicative

added def OrderMonoidIso.toAdditive

added def OrderMonoidIso.toMultiplicative_toAdditive

Created Mathlib/Algebra/Order/Monoid/LocallyFiniteOrder.lean

added theorem Finset.card_Ico_mul_right

added def LocallyFiniteOrder.addMonoidHom

added def LocallyFiniteOrder.orderAddMonoidEquiv

added theorem LocallyFiniteOrder.orderAddMonoidEquiv_apply

added def LocallyFiniteOrder.orderAddMonoidHom

added theorem LocallyFiniteOrder.orderAddMonoidHom_apply

added theorem LocallyFiniteOrder.orderAddMonoidHom_bijective

added theorem LocallyFiniteOrder.orderAddMonoidHom_strictMono

added theorem LocallyFiniteOrder.orderAddMonoidHom_toAddMonoidHom

added def LocallyFiniteOrder.orderMonoidEquiv

added def LocallyFiniteOrder.orderMonoidHom

added theorem LocallyFiniteOrder.orderMonoidHom_strictMono

added def LocallyFiniteOrder.orderMonoidWithZeroEquiv

added def LocallyFiniteOrder.orderMonoidWithZeroHom

added theorem LocallyFiniteOrder.orderMonoidWithZeroHom_strictMono

added theorem card_Ico_one_mul

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

deleted def OrderAddMonoidIso.toAdditive_toMultiplicative

deleted def OrderAddMonoidIso.toMultiplicative''

deleted def OrderAddMonoidIso.toMultiplicative'

deleted def OrderAddMonoidIso.toMultiplicative

deleted def OrderMonoidIso.toAdditive

deleted def OrderMonoidIso.toMultiplicative_toAdditive