Theorems · Definition · group theory

Con.lift

{M : Type u_1} →
  {P : Type u_3} →
    [inst : MulOneClass M] → [inst_1 : MulOneClass P] → (c : Con M) → (f : M →* P) → c ≤ Con.ker f → c.Quotient →* P

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

Defined in

Mathlib.GroupTheory.Congruence.Hom

Cited by

12 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound

Assumes

MulOneClassMulOneClass