Theorems · Definition · group theory

AddCon.lift

{M : Type u_1} →
  {P : Type u_3} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass P] → (c : AddCon M) → (f : M →+ P) → c ≤ AddCon.ker f → c.Quotient →+ P

The homomorphism on the quotient of an AddMonoid by an additive congruence relation c induced by a homomorphism constant on c's equivalence classes.

Defined in

Mathlib.GroupTheory.Congruence.Hom

Cited by

14 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound

Assumes

AddZeroClassAddZeroClass