Theorems · Theorem · order theory

FiniteMulArchimedeanClass.lift.congr_simp

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

Defined in

Mathlib.Algebra.Order.Archimedean.Class

Cited by

0 results in Mathlib

Foundations

Depth 41 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommGroupLinearOrderIsOrderedMonoid