coprod_apply — Mathlib

English

Let f: M →* P and g: N →* P be monoid homomorphisms into a commutative monoid P. For every (m, n) ∈ M × N, the coproduct map satisfies (f ⊔ g)(m, n) = f(m) g(n).

Русский

Пусть f: M →* P и g: N →* P — моноид-гомоморфизмы в коммутативный моноид P. Для каждого элемента (m, n) ∈ M × N выполняется (f coprod g)(m, n) = f(m) g(n).

LaTeX

$$$\\forall f:M \\to P,\\ \\forall g:N \\to P,\\ \\forall (m,n) \\in M \\times N:\\ (f \\coprod g)(m,n) = f(m)\\,g(n).$$$

Lean4

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

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