English
There is a left module structure of the opposite matrix algebra (M_n(R))^op on the vector space R^n, defined by A^op · v := v^T A (i.e., row-vector multiplication by A). The standard module axioms hold: 1 · v = v, (A+B) · v = A · v + B · v, A · (v+w) = A · v + A · w, and (A B) · v = A · (B · v).
Русский
Существует лево-модульная структура противо-алгебры матриц (M_n(R))^op над пространством столбцовых векторов R^n, заданная \(A^{op} \cdot v = v^T A\) (множение строк-вектора на матрицу). Аксиомы модуля выполняются: 1·v=v, (A+B)·v=A·v+B·v, A·(v+w)=A·v+A·w, (A B)·v=A·(B·v).
LaTeX
$$$\\text{There is a left }(M_n(R))^{op}\\text{-module on } R^n\\text{ given by } A^{op} \\cdot v := v^{\\top} A$$$
Lean4
instance : Module (Matrix n n R)ᵐᵒᵖ (n → R) where
smul A v := v ᵥ* A.unop
one_smul := Matrix.vecMul_one
mul_smul _ _ _ := (vecMul_vecMul _ _ _).symm
zero_smul := vecMul_zero
add_smul _ _ := vecMul_add _ _
smul_zero _ := zero_vecMul _
smul_add _ := add_vecMul _
