Theorems · Definition · order theory

FiniteMulArchimedeanClass

(M : Type u_1) → [inst : CommGroup M] → [inst_1 : LinearOrder M] → [IsOrderedMonoid M] → Type (max 0 u_1)

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.

Defined in

Mathlib.Algebra.Order.Archimedean.Class

Cited by

21 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommGroupLinearOrderIsOrderedMonoid