Theorems · Definition · group theory

Monoid.PushoutI

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

The indexed pushout of monoids, which is the pushout in the category of monoids, or the category of groups.

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

30 results in Mathlib

Foundations

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

Assumes

MonoidMonoid