Theorems · Theorem · group theory

Monoid.CoprodI.ext_hom

∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {N : Type u_3} [inst_1 : Monoid N]
  (f g : Monoid.CoprodI M →* N), (∀ (i : ι), f.comp Monoid.CoprodI.of = g.comp Monoid.CoprodI.of) → f = g

See note [partially-applied ext lemmas].

Defined in

Mathlib.GroupTheory.CoprodI

Cited by

2 results in Mathlib

Foundations

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

Assumes

MonoidMonoid