vecMulVec_smul — Mathlib

English

For any r, w, v with [Semiring α], vecMulVec w (r • v) = r • vecMulVec w v.

Русский

Для любого r, w, v над полем/кольцом α выполняется vecMulVec w (r • v) = r • vecMulVec w v.

LaTeX

$$vecMulVec w (r \\cdot v) = r \\cdot vecMulVec w v$$

Lean4

@[simp]
theorem vecMulVec_smul [Mul α] [SMul R α] [SMulCommClass R α α] (r : R) (w : m → α) (v : n → α) :
    vecMulVec w (r • v) = r • vecMulVec w v :=
  ext fun _ _ => mul_smul_comm _ _ _

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