op_smul_eq_vecMul — Mathlib

English

For A in the opposite matrix algebra and any vector v, the action is given by the standard row-vector times matrix product: A • v = v^T A.

Русский

Для A из противоположной матричной алгебры и вектора v действует обычное умножение строки на матрицу: A • v = v^T A.

LaTeX

$$$A \\cdot v = v^{\\top} A$$$

Lean4

@[simp]
theorem op_smul_eq_vecMul (A : (Matrix n n R)ᵐᵒᵖ) (v : n → R) : A • v = v ᵥ* A.unop :=
  rfl

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