Theorems · Theorem · group theory

Units.coe_liftRight

∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] {f : M →* N} {g : M → Nˣ}
  (h : ∀ (x : M), ↑(g x) = f x) (x : M), ↑((Units.liftRight f g h) x) = f x

Defined in

Mathlib.Algebra.Group.Units.Hom

Cited by

4 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

MonoidMonoid