English
Any nontrivial locally finite linearly ordered abelian group G is isomorphic to the integers: there exists an order-preserving additive monoid isomorphism from G onto ℤ.
Русский
Любая ненулевая локально конечная линейно упорядоченная абелева группа G изотропна к целым числам: существует порядок-сохраняющий моноидный изоморфизм G ≅ ℤ.
LaTeX
$$$\text{There exists an order-preserving additive monoid isomorphism } G \cong_{o} \mathbb{Z}$$$
Lean4
/-- Any nontrivial linearly ordered abelian group that is locally finite is isomorphic to `ℤ`. -/
noncomputable def orderAddMonoidEquiv [Nontrivial G] : G ≃+o ℤ
where
__ := orderAddMonoidHom G
__ := AddEquiv.ofBijective (orderAddMonoidHom G) orderAddMonoidHom_bijective
map_le_map_iff'
{a b} := by
obtain ⟨b, rfl⟩ := add_left_surjective a b
suffices 0 ≤ orderAddMonoidHom G b ↔ 0 ≤ b by simpa
obtain hb | hb := le_total 0 b
· simp [orderAddMonoidHom, addMonoidHom, hb]
· simp [orderAddMonoidHom, addMonoidHom, hb]
