Theorems · Theorem · group theory

QuotientGroup.monoidHom_ext

∀ {G : Type u_1} {M : Type u_4} [inst : Group G] [inst_1 : Monoid M] (N : Subgroup G) [nN : N.Normal]
  ⦃f g : G ⧸ N →* M⦄, f.comp (QuotientGroup.mk' N) = g.comp (QuotientGroup.mk' N) → f = g

Two MonoidHoms from a quotient group are equal if their compositions with QuotientGroup.mk' are equal. See note [partially-applied ext lemmas].

Defined in

Mathlib.GroupTheory.QuotientGroup.Defs

Cited by

5 results in Mathlib

Foundations

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

Assumes

GroupMonoidSubgroup.Normal