Theorems · Theorem · order theory

MulArchimedeanClass.mk_eq_mk

∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk a = MulArchimedeanClass.mk b ↔ (∃ m, |b|ₘ ≤ |a|ₘ ^ m) ∧ ∃ n, |a|ₘ ≤ |b|ₘ ^ n

Defined in

Mathlib.Algebra.Order.Archimedean.Class

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommGroupLinearOrderIsOrderedMonoid