English
Let n be finite and R a semiring. Let S act on R via a distributive scalar action and suppose the scalar action is compatible with itself (a scalar tower S → R → R). Then the natural action of S on the matrix ring M_n(R) and on the column vectors R^n is compatible with matrix-vector multiplication, i.e., for all s in S, A in M_n(R), and v in R^n, s · (A · v) = (s · A) · v.
Русский
Пусть n — конечный множитель, R — полугруппа; пусть S действует на R через распределимое скалярное действие и выполняется условие совместимости действий (скалярная башня S → R → R). Тогда естественное действие S на кольцо матриц M_n(R) и на векторы-столбцы R^n совместимо с умножением матрица на вектор: для всех s ∈ S, A ∈ M_n(R) и v ∈ R^n выполняется s · (A · v) = (s · A) · v.
LaTeX
$$$\\forall s \\in S,\\ A \\in M_n(R),\\ v \\in R^n:\\ s \\cdot (A \\cdot v) = (s \\cdot A) \\cdot v$$$
Lean4
instance [DistribSMul S R] [IsScalarTower S R R] : IsScalarTower S (Matrix n n R) (n → R) where
smul_assoc := smul_mulVec
