Theorems · Theorem · group theory

Con.hom_ext

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

Homomorphisms on the quotient of a monoid by a congruence relation c are equal if their compositions with c.mk' are equal.

Defined in

Mathlib.GroupTheory.Congruence.Hom

Cited by

3 results in Mathlib

Foundations

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

Assumes

MulOneClassMulOneClass