Theorems · Theorem · order theory

MulArchimedeanClass.lift.congr_simp

∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {α : Type u_2}
  (f f_1 : M → α) (e_f : f = f_1) (h : ∀ (a b : M), MulArchimedeanClass.mk a = MulArchimedeanClass.mk b → f a = f b)
  (a a_1 : MulArchimedeanClass M), a = a_1 → MulArchimedeanClass.lift f h a = MulArchimedeanClass.lift f_1 ⋯ a_1

Defined in

Mathlib.Algebra.Order.Archimedean.Class

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommGroupLinearOrderIsOrderedMonoid