English
The archimedean class of an element a ∈ M is the equivalence class under the Archimedean relation, i.e., mk a and mk b are identified iff a and b dominate each other via some powers.
Русский
Архимедово класс элемента a ∈ M определяется как эквивалентность по отношению Архимедова, то есть mk a и mk b эквивалентны, если a и b взаимно доминируют через некоторую мощность.
LaTeX
$$$\text{MulArchimedeanClass } M = \text{Antisymmetrization}(\text{MulArchimedeanOrder } M, \le)$.$$
Lean4
/-- `MulArchimedeanClass M` is the quotient of the group `M` by multiplicative archimedean
equivalence, where two elements `a` and `b` are in the same class iff
`(∃ m : ℕ, |b|ₘ ≤ |a|ₘ ^ m) ∧ (∃ n : ℕ, |a|ₘ ≤ |b|ₘ ^ n)`. -/
@[to_additive ArchimedeanClass /--
`ArchimedeanClass M` is the quotient of the additive group `M` by additive archimedean
equivalence, where two elements `a` and `b` are in the same class iff
`(∃ m : ℕ, |b| ≤ m • |a|) ∧ (∃ n : ℕ, |a| ≤ n • |b|)`. -/
]
def MulArchimedeanClass :=
Antisymmetrization (MulArchimedeanOrder M) (· ≤ ·)
