Theorems · Definition · order theory

ArchimedeanClass

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

ArchimedeanClass M is the quotient 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|).

Defined in

Mathlib.Algebra.Order.Archimedean.Class

Cited by

247 results in Mathlib

Foundations

Depth 21 from the axioms, rests on 241 definitions · uses propext, Quot.sound

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoid