English
For any non-identity element a in a commutative group M with a linear order and an ordered monoid structure, there is a finite Archimedean class associated to a, given by the constructor mk(a, h) where h ≠ 1.
Русский
Для любого элементa a в коммутативной группе M с линейным порядком и структурой упорядоченного моноида существует конечный Архимедов класс, связанный с a, задаваемый конструктором mk(a, h) при ha ≠ 1.
LaTeX
$$$\text{FiniteMulArchimedeanClass.mk } a\; h = \langle MulArchimedeanClass.mk a, MulArchimedeanClass.mk_eq_top_iff.not.mpr h \rangle$$$
Lean4
/-- Create a `FiniteMulArchimedeanClass` from a non-one element. -/
@[to_additive /-- Create a `FiniteArchimedeanClass` from a non-zero element. -/
]
def mk (a : M) (h : a ≠ 1) : FiniteMulArchimedeanClass M :=
⟨MulArchimedeanClass.mk a, MulArchimedeanClass.mk_eq_top_iff.not.mpr h⟩
