English
A matrix acts on a column vector to produce another vector, and this action satisfies the module axioms with scalar multiplication by the base ring.
Русский
Матрица действует на столбцовый вектор, образуя другой вектор, и это действие удовлетворяет аксиомам модуля над кольцом-основанием.
LaTeX
$$$\text{The action }(A:\mathrm{Matrix}\ n\ n\ R)\ \text{on }(v:\ n\to R)\text{ given by }A\cdot v\text{ satisfies the module axioms with scalars in }R$$$
Lean4
instance : Module (Matrix n n R) (n → R) where
smul := mulVec
one_smul := one_mulVec
mul_smul _ _ _ := (mulVec_mulVec _ _ _).symm
zero_smul := zero_mulVec
add_smul := add_mulVec
smul_zero := mulVec_zero
smul_add := mulVec_add
