English
For hs ≠ ⊤, a ∈ subgroup s iff mk a ∈ s; equivalently, membership transfers between M and MulArchimedeanClass.
Русский
Для hs ≠ ⊤, a ∈ subgroup s эквивалентно mk a ∈ s; членство переносится между M и MulArchimedeanClass.
LaTeX
$$$hs \\neq \\top \\Rightarrow (a \\in subgroup s \\iff mk(a) \\in s)$$$
Lean4
/-- `FiniteMulArchimedeanClass M` is the quotient of the non-one elements 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)`.
It is defined as the subtype of non-top elements of `MulArchimedeanClass M`
(`⊤ : MulArchimedeanClass M` is the archimedean class of `1`).
This is useful since the family of non-top archimedean classes is linearly independent. -/
@[to_additive FiniteArchimedeanClass /--
`FiniteArchimedeanClass M` is the quotient of the non-zero elements 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|)`.
It is defined as the subtype of non-top elements of `ArchimedeanClass M`
(`⊤ : ArchimedeanClass M` is the archimedean class of `0`).
This is useful since the family of non-top archimedean classes is linearly independent. -/
]
abbrev FiniteMulArchimedeanClass :=
{ A : MulArchimedeanClass M // A ≠ ⊤ }
