Theorems · Theorem · group theory

AddCon.lift_funext

∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M}
  (f g : c.Quotient →+ P), (∀ (a : M), f ↑a = g ↑a) → f = g

Homomorphisms on the quotient of an AddMonoid by an additive congruence relation are equal if they are equal on elements that are coercions from the AddMonoid.

Defined in

Mathlib.GroupTheory.Congruence.Hom

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddZeroClassAddZeroClass