Theorems · Definition · order theory

MulArchimedeanClass

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

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).

Defined in

Mathlib.Algebra.Order.Archimedean.Class

Cited by

81 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

CommGroupLinearOrderIsOrderedMonoid