Theorems · Theorem · group theory

AddCon.hom_ext

∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M}
  {f g : c.Quotient →+ P}, f.comp c.mk' = g.comp c.mk' → f = g

Homomorphisms on the quotient of an AddMonoid by an additive congruence relation c are equal if their compositions with c.mk' are equal.

Defined in

Mathlib.GroupTheory.Congruence.Hom

Cited by

5 results in Mathlib

Foundations

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

Assumes

AddZeroClassAddZeroClass