English
Any nontrivial locally finite, linearly ordered abelian group G is isomorphic to ℤ as an ordered additive group; the construction orderAddMonoidEquiv G provides this isomorphism.
Русский
Любая ненулевая локально конечная линейно упорядоченная абелева группа G изоморфна к целым числам как упорядоченная абелева группа; конструкция orderAddMonoidEquiv G задаёт этот изоморфизм.
LaTeX
$$$\exists \phi: G \to_o \mathbb{Z}\,$, где $\phi$ является исоморфизмом порядков и аддитивной структурой.$$
Lean4
/-- Any linearly ordered abelian group that is locally finite embeds to `Multiplicative ℤ`. -/
noncomputable def orderMonoidEquiv (G : Type*) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [LocallyFiniteOrder G]
[Nontrivial G] : G ≃*o Multiplicative ℤ :=
have : LocallyFiniteOrder (Additive G) := ‹LocallyFiniteOrder G›
(orderAddMonoidEquiv (Additive G)).toMultiplicative
