Theorems · Definition · order theory

FiniteArchimedeanClass

(M : Type u_1) → [inst : AddCommGroup M] → [inst_1 : LinearOrder M] → [IsOrderedAddMonoid M] → Type (max 0 u_1)

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.

Defined in

Mathlib.Algebra.Order.Archimedean.Class

Cited by

100 results in Mathlib

Foundations

Depth 32 from the axioms, rests on 375 definitions · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoid