English
For a commutative linearly ordered group with archimedean property, the least element of the positive part of the closure of a is exactly the element |a|_m, and this is the unique least element greater than 1.
Русский
В коммутативной линейно упорядоченной группе с архимедеевостью наименьший элемент в положительной части замыкания элемента a равен |a|_м и является единственным наименьшим >1.
LaTeX
$$$ IsLeast\{ y \in closure(\{a\}) \mid 1 < y \} = (y = |a|_m) \land (1 < y). $$$
Lean4
@[to_additive]
theorem isLeast_of_closure_iff_eq_mabs {a b : G} :
IsLeast {y : G | y ∈ closure ({ a } : Set G) ∧ 1 < y} b ↔ b = |a|ₘ ∧ 1 < b :=
by
constructor <;> intro h
· have := Subgroup.cyclic_of_min h
have ha : a ∈ closure ({ b } : Set G) := by simp [← this]
rw [mem_closure_singleton] at ha
obtain ⟨n, rfl⟩ := ha
have := h.left
simp only [mem_closure_singleton, mem_setOf_eq] at this
obtain ⟨m, hm⟩ := this.left
have key : m * n = 1 := by rw [← zpow_right_inj this.right, zpow_mul', hm, zpow_one]
rw [Int.mul_eq_one_iff_eq_one_or_neg_one] at key
rw [eq_comm]
rcases key with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ <;> simp [this.right.le, this.right, mabs]
· wlog ha : 1 ≤ a generalizing a
· convert @this (a⁻¹) ?_ (by simpa using le_of_not_ge ha) using 4
· simp
· rwa [mabs_inv]
rw [mabs, sup_eq_left.mpr ((inv_le_one'.mpr ha).trans ha)] at h
rcases h with ⟨rfl, h⟩
refine ⟨?_, ?_⟩
· simp [h]
· intro x
simp only [mem_closure_singleton, mem_setOf_eq, and_imp, forall_exists_index]
rintro k rfl hk
rw [← zpow_one b, ← zpow_mul, one_mul, zpow_le_zpow_iff_right h, ← zero_add 1, ← Int.lt_iff_add_one_le]
contrapose! hk
rw [← Left.one_le_inv_iff, ← zpow_neg]
exact one_le_zpow ha (by simp [hk])
