smul_tprod_mul_smul_tprod — Mathlib

English

For r, s in the base ring R and x, y in Π i, A_i, we have (r • tprod R x) * (s • tprod R y) = (r s) • tprod R (x * y).

Русский

Для элементов r, s из R и x, y из Π_i A_i выполняется (r • tprod R x) · (s • tprod R y) = (r s) • tprod R (x y).

LaTeX

$$$(r\\ \\cdot\\ tprod\\ R\\ x)\\ *\\ (s\\ \\cdot\\ tprod\\ R\\ y) = (r\\ s)\\ \\cdot\\ tprod\\ R\\ (x\\ *\\ y)$$$

Lean4

theorem smul_tprod_mul_smul_tprod (r s : R) (x y : Π i, A i) :
    (r • tprod R x) * (s • tprod R y) = (r * s) • tprod R (x * y) := by
  simp only [mul_def, map_smul, LinearMap.smul_apply, mul_tprod_tprod, mul_comm r s, mul_smul]

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