English
Let M be a commutative group with a linear order and an ordered monoid structure. If every nontrivial element lies in the same multiplicative Archimedean class, i.e. mk(a) = mk(b) for all a ≠ 1 and b ≠ 1, then M carries a multiplicative Archimedean structure.
Русский
Пусть M — коммутативная группа с линейным порядком и структурой упорядоченного моноида. Если все ненулевые элементы принадлежат одному и тому же мультипликативному Архимедовому классу, то на M существует Архимедова структура в мультипликативном смысле.
LaTeX
$$$\\Big( \\forall a \\neq 1, \\forall b \\neq 1, \\ mk(a) = mk(b) \\Big) \\Rightarrow \\MulArchimedean M$$$
Lean4
@[to_additive archimedean_of_mk_eq_mk]
theorem mulArchimedean_of_mk_eq_mk (h : ∀ a ≠ (1 : M), ∀ b ≠ 1, mk a = mk b) : MulArchimedean M where
arch x y
hy := by
by_cases hx : x ≤ 1
· use 0
simpa using hx
· have hx : 1 < x := lt_of_not_ge hx
have hxy : mk x = mk y := h x hx.ne.symm y hy.ne.symm
obtain ⟨_, ⟨m, hm⟩⟩ := (mk_eq_mk).mp hxy
rw [mabs_eq_self.mpr hx.le, mabs_eq_self.mpr hy.le] at hm
exact ⟨m, hm⟩
