English
Equivalent restatements show that the least element of the closure corresponds to the multiplicative absolute value, with a precise equivalence condition.
Русский
Эквивалентные формулировки показывают, что наименьший элемент замыкания соответствует мультипликативному модулю, с точным условием эквивалентности.
LaTeX
$$$ IsLeast\{ y \mid y \in closure(\{a\}) \land 1 < y\} b \leftrightarrow b = |a|_m \land 1 < b $$$
Lean4
/-- If an element of a linearly ordered archimedean additive group is the least positive element,
then the whole group is isomorphic (and order-isomorphic) to the integers. -/
noncomputable def int_orderAddMonoidIso_of_isLeast_pos {G : Type*} [AddCommGroup G] [LinearOrder G]
[IsOrderedAddMonoid G] [Archimedean G] {x : G} (h : IsLeast {y : G | 0 < y} x) : G ≃+o ℤ :=
by
have : IsLeast {y : G | y ∈ (⊤ : AddSubgroup G) ∧ 0 < y} x := by simpa using h
replace this := AddSubgroup.cyclic_of_min this
let e : G ≃+o (⊤ : AddSubgroup G) :=
⟨AddSubsemigroup.topEquiv.symm, (AddEquiv.strictMono_symm AddSubsemigroup.strictMono_topEquiv).le_iff_le⟩
let e' : (⊤ : AddSubgroup G) ≃+o AddSubgroup.closure { x } :=
⟨AddEquiv.subsemigroupCongr (by simp [this]), (AddEquiv.strictMono_subsemigroupCongr _).le_iff_le⟩
let g : (⊤ : AddSubgroup ℤ) ≃+o ℤ := ⟨AddSubsemigroup.topEquiv, (AddSubsemigroup.strictMono_topEquiv).le_iff_le⟩
let g' : AddSubgroup.closure ({ 1 } : Set ℤ) ≃+o (⊤ : AddSubgroup ℤ) :=
⟨(.subsemigroupCongr (by simp)), (AddEquiv.strictMono_subsemigroupCongr _).le_iff_le⟩
let f := closure_equiv_closure x (1 : ℤ) (by simp [h.left.ne'])
exact ((((e.trans e').trans f).trans g').trans g : G ≃+o ℤ)
