Theorems · Theorem · group theory

Units.liftRight_inv_mul

∀ {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 = 1

Defined in

Mathlib.Algebra.Group.Units.Hom

Cited by

1 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext

Assumes

MonoidMonoid