Theorems · Definition · group theory

Monoid.PushoutI.ofCoprodI

{ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Monoid (G i)] →
        [inst_1 : Monoid H] → {φ : (i : ι) → H →* G i} → Monoid.CoprodI G →* Monoid.PushoutI φ

The map from the coproduct into the pushout

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

8 results in Mathlib

Foundations

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

Assumes

MonoidMonoid