Theorems · Theorem · order theory

FiniteMulArchimedeanClass.lift_mk

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

Defined in

Mathlib.Algebra.Order.Archimedean.Class

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommGroupLinearOrderIsOrderedMonoid