Theorems · Theorem · group theory

Monoid.PushoutI.hom_ext_iff

∀ {ι : 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},
  f = g ↔
    (∀ (i : ι), f.comp (Monoid.PushoutI.of i) = g.comp (Monoid.PushoutI.of i)) ∧
      f.comp (Monoid.PushoutI.base φ) = g.comp (Monoid.PushoutI.base φ)

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

0 results in Mathlib

Foundations

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

Assumes

MonoidMonoidMonoid