Theorems · Theorem · group theory

Abelianization.hom_ext

∀ {G : Type u} [inst : Group G] {A : Type v} [inst_1 : Monoid A] (φ ψ : Abelianization G →* A),
  φ.comp Abelianization.of = ψ.comp Abelianization.of → φ = ψ

See note [partially-applied ext lemmas].

Defined in

Mathlib.GroupTheory.Abelianization.Defs

Cited by

4 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupMonoid