English
Any nontrivial linearly ordered abelian group G with locally finite order admits an order-preserving monoid isomorphism to the multiplicative group of integers: an isomorphism G ≃*o ℤ.
Русский
Любая ненулевая линейно упорядоченная абелева группа G с локально конечным порядком допускает порядок-моноидный изоморфизм к множителю целых чисел: G ≃*o ℤ.
LaTeX
$$$G \cong_{*o} \mathbb{Z}$$$
Lean4
/-- Any linearly ordered abelian group that is locally finite embeds into `Multiplicative ℤ`. -/
noncomputable def orderMonoidHom (G : Type*) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [LocallyFiniteOrder G] :
G →*o Multiplicative ℤ :=
have : LocallyFiniteOrder (Additive G) := ‹LocallyFiniteOrder G›
⟨(orderAddMonoidHom (Additive G)).toMultiplicative, (orderAddMonoidHom (Additive G)).2⟩
