English
The Monoid CoprodI is the free product (categorical coproduct) of an indexed family (M_i) of monoids; its elements can be described as words built from elements of the various M_i with concatenation as multiplication.
Русский
Monoid CoprodI есть свободный копродукт семейства моноидов M_i; элементы можно описать словами, составленными из элементов M_i разных индексов, с умножением как конкатенацией.
LaTeX
$$$\\mathrm{CoprodI}(M) \\text{ is the coproduct in Monoids, with a word-based description for its elements and universal property.}$$$
Lean4
/-- The free product (categorical coproduct) of an indexed family of monoids. -/
def CoprodI : Type _ :=
(conGen (Monoid.CoprodI.Rel M)).Quotient
deriving Monoid, Inhabited
