vecMul_one — Mathlib

English

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

Русский

Для u,v,w,x ∈ α^m выполняется 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

@[simp]
theorem vecMul_one (v : m → α) : v ᵥ* 1 = v := by
  ext
  rw [← diagonal_one, vecMul_diagonal, mul_one]

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