English
A repeated instance of the compatibility: (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g).
Русский
Повторение совместимости: (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g).
LaTeX
$$$ (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g). $$$
Lean4
/-- Coproduct of two `MonoidHom`s with the same codomain:
`f.coprod g (p : M × N) = f p.1 * g p.2`.
(Commutative case; for the general case, see `MonoidHom.noncommCoprod`.) -/
@[to_additive /-- Coproduct of two `AddMonoidHom`s with the same codomain:
`f.coprod g (p : M × N) = f p.1 + g p.2`.
(Commutative case; for the general case, see `AddHom.noncommCoprod`.) -/
]
def coprod : M × N →* P :=
f.comp (fst M N) * g.comp (snd M N)
