vecMul_transpose — Mathlib

English

Let A ∈ M_{m×n}(α) and x ∈ α^n. Then x ᵥ* Aᵀ = A.mulVec x, expressing that left-multiplication by a row-vector and right-multiplication by a transpose agree with the standard vecMul.

Русский

Пусть A ∈ M_{m×n}(α) и x ∈ α^n. Тогда x ᵥ* Aᵀ = A.mulVec x, т.е. левая умножение строковым вектором совпадает с обычным vecMul.

LaTeX

$$$ x ᵥ* A^\\top = A.mulVec x $$$

Lean4

theorem vecMul_transpose [Fintype n] (A : Matrix m n α) (x : n → α) : x ᵥ* Aᵀ = A *ᵥ x :=
  by
  ext
  apply dotProduct_comm

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