tprod_mul_tprod — Mathlib

English

For x, y functions on ι-valued tuples, the tensor product respects multiplication: tprod R x * tprod R y = tprod R (x * y).

Русский

Для x, y функций над кортежами ι， тензорное произведение сохраняет умножение: tprod R x * tprod R y = tprod R (x * y).

LaTeX

$$tprod R x * tprod R y = tprod R (x * y)$$

Lean4

@[simp]
theorem tprod_mul_tprod (x y : (i : ι) → A i) : tprod R x * tprod R y = tprod R (x * y) :=
  mul_tprod_tprod x y

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