Theorems · Definition · group theory

IsAddUnit.liftRight

{M : Type u_3} →
  {N : Type u_4} →
    [inst : AddMonoid M] → [inst_1 : AddMonoid N] → (f : M →+ N) → (∀ (x : M), IsAddUnit (f x)) → M →+ AddUnits N

If a homomorphism f : M →+ N sends each element to an IsAddUnit, then it can be lifted to f : M →+ AddUnits N. See also AddUnits.liftRight for a computable version.

Defined in

Mathlib.Algebra.Group.Units.Hom

Cited by

25 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Classical.choice

Assumes

AddMonoidAddMonoid