vecMulVec_mul_vecMulVec — Mathlib

English

For Fintype m and vectors u,v,w,x, the product vecMulVec u v with vecMulVec w x equals vecMulVec u ((v ⬝ᵥ w) • x).

Русский

Для u,v,w,x ∈ α^м имеем vecMulVec u v · vecMulVec w x = vecMulVec u ((v ⬝ᵥ w) • x).

LaTeX

$$$\operatorname{vecMulVec} u v \; \cdot \operatorname{vecMulVec} w x = \operatorname{vecMulVec} u\big((v \;⬝ᵥ\; w) \;•\; x\big)$$$

Lean4

theorem vecMulVec_mul_vecMulVec [Fintype m] (u : l → α) (v w : m → α) (x : n → α) :
    vecMulVec u v * vecMulVec w x = vecMulVec u ((v ⬝ᵥ w) • x) := by rw [vecMulVec_mul, vecMul_vecMulVec]

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