coe_prod — Mathlib

English

The product of two linear maps f: M → M₂ and g: M → M₃ is the linear map M → M₂ × M₃ sending x to (f x, g x).

Русский

Произведение двух линейных отображений f: M → M₂ и g: M → M₃ задаёт линейное отображение M → M₂ × M₃, отправляющее x в (f x, g x).

LaTeX

$$$\text{prod}(f,g): M\to M_2\times M_3$, $\text{toFun}(x)=(f(x),g(x))$ with linearity in x.$$

Lean4

theorem coe_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : ⇑(f.prod g) = Pi.prod f g :=
  rfl

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