mulVec_transpose — Mathlib

English

For finite index m and matrices A ∈ M_{m×n}(α) and vector x ∈ α^n, the relation Aᵀ x = xᵀ A holds, expressing the compatibility of transpose with vecMul.

Русский

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

LaTeX

$$$A^\\top x = x^\\top A$$$

Lean4

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

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