English
Let M be a commutative group equipped with a linear order compatible with multiplication (i.e., an ordered monoid). For any a, b in M, the Archimedean class of a is less than or equal to that of b exactly when there exists a natural number n such that the magnitude of b is at most the magnitude of a raised to the nth power: mk(a) ≤ mk(b) iff ∃ n ∈ N, |b|_m ≤ |a|_m^n.
Русский
Пусть M — коммутативная группа, оснащенная линейным порядком, совместимым с умножением (упорядоченный моноид). Для любых a, b ∈ M верно: класс Архимедова множества a не превосходит класс Архимедова множества b тогда и только тогда, когда существует натуральное n такое, что |b|_м ≤ |a|_м^n: mk(a) ≤ mk(b) ⇔ ∃ n ∈ N, |b|_м ≤ |a|_м^n.
LaTeX
$$$mk\ a \le mk\ b \iff \exists n \in \mathbb{N},\ |b|_m \le |a|_m^n$$$
Lean4
@[to_additive]
theorem mk_le_mk : mk a ≤ mk b ↔ ∃ n, |b|ₘ ≤ |a|ₘ ^ n :=
.rfl
