coe_prod — Mathlib

English

The product of two monoid homomorphisms is defined by toFun = (x ↦ (f x, g x)) and respects multiplication.

Русский

Произведение двух моноид-гомоморфизмов определяется функцией, задающей x ↦ (f x, g x), и сохраняет умножение.

LaTeX

$$$\mathrm{MulHom}.prod(f,g)$ is the map $x\mapsto (f(x),g(x))$ and is a monoid homomorphism.$$

Lean4

@[to_additive coe_prod]
theorem coe_prod (f : M →ₙ* N) (g : M →ₙ* P) : ⇑(f.prod g) = Pi.prod f g :=
  rfl

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