prod — Mathlib

English

The underlying function of the product map f.prod g equals the product of the underlying functions f and g.

Русский

Базовая функция отображения $f.oplus g$ равна произведению функций $f$ и $g$.

LaTeX

$$$\bigl\langle f,g\bigr\rangle_{\text{prod}} = \mathrm{Pi}.prod (f,g).$$

Lean4

/-- The prod of two linear maps is a linear map. -/
@[simps]
def prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : M →ₗ[R] M₂ × M₃
    where
  toFun := Pi.prod f g
  map_add' x y := by simp only [Pi.prod, Prod.mk_add_mk, map_add]
  map_smul' c x := by simp only [Pi.prod, Prod.smul_mk, map_smul, RingHom.id_apply]

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