Theorems · Theorem · group theory

Monoid.PushoutI.hom_ext

∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [inst : Monoid K] [inst_1 : (i : ι) → Monoid (G i)]
  [inst_2 : Monoid H] {φ : (i : ι) → H →* G i} {f g : Monoid.PushoutI φ →* K},
  (∀ (i : ι), f.comp (Monoid.PushoutI.of i) = g.comp (Monoid.PushoutI.of i)) →
    f.comp (Monoid.PushoutI.base φ) = g.comp (Monoid.PushoutI.base φ) → f = g

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

2 results in Mathlib

Foundations

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

Assumes

MonoidMonoidMonoid