vecMulVec_mul — Mathlib

English

For Fintype m, x ∈ α^l, y ∈ α^m and M ∈ M(m,n;α), vecMulVec x y · M = vecMulVec x (y ᵥ* M).

Русский

Для x ∈ α^l, y ∈ α^m и M ∈ M(m,n;α) имеем vecMulVec x y · M = vecMulVec x (y ᵥ* M).

LaTeX

$$$\operatorname{vecMulVec} x y \; M = \operatorname{vecMulVec} x (y ᵥ* M)$$$

Lean4

theorem vecMulVec_mul [Fintype m] (x : l → α) (y : m → α) (M : Matrix m n α) :
    vecMulVec x y * M = vecMulVec x (y ᵥ* M) := by
  ext
  simp_rw [mul_apply, vecMulVec_apply, vecMul, dotProduct, Finset.mul_sum, mul_assoc]

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