Theorems · Theorem · group theory

AddCon.ker_eq_lift_of_injective

∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] (c : AddCon M) (f : M →+ P)
  (H : c ≤ AddCon.ker f), Function.Injective ⇑(c.lift f H) → AddCon.ker f = c

Given an AddMonoid homomorphism f from M to P, the kernel of f is the unique additive congruence relation on M whose induced map from the quotient of M to P is injective.

Defined in

Mathlib.GroupTheory.Congruence.Hom

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Quot.sound

Assumes

AddZeroClassAddZeroClass