English
Compatibility of prod with maps: the composition of prod with prodMap equals the product of compositions.
Русский
Совместимость prod с prodMap: составление prod с prodMap равно произведению композиционных отображений.
LaTeX
$$$ (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g) $$$
Lean4
/-- Coproduct of two `MulHom`s with the same codomain:
`f.coprod g (p : M × N) = f p.1 * g p.2`.
(Commutative codomain; for the general case, see `MulHom.noncommCoprod`) -/
@[to_additive /-- Coproduct of two `AddHom`s with the same codomain:
`f.coprod g (p : M × N) = f p.1 + g p.2`.
(Commutative codomain; for the general case, see `AddHom.noncommCoprod`) -/
]
def coprod : M × N →ₙ* P :=
f.comp (fst M N) * g.comp (snd M N)
