coprod_apply — Mathlib

English

Coproduct of two MulHom f: M → P and g: N → P with commutative codomain P: f.coprod g: M × N → P given by f(p1) · g(p2).

Русский

Копродукт двух MulHom f: M → P и g: N → P, где кодом P является коммутативный полугрупп, задаёт отображение f.coprod g: M×N → P, и оно даётся формулой f(p1)·g(p2).

LaTeX

$$$f.coprod g = f \circ \mathrm{fst} \; * \; g \circ \mathrm{snd}$$$

Lean4

@[to_additive (attr := simp)]
theorem coprod_apply (p : M × N) : f.coprod g p = f p.1 * g p.2 :=
  rfl

Похожие утверждения