instSMulCommClassMulOppositeForallOfIsScalarTower_1

English

The actions of S and MulOpposite(Matrix n n R) on column vectors commute uniformly; i.e., for all s, A, v the two actions can be interchanged without changing the result.

Русский

Действия S и MulOpposite(Matrix n n R) на векторах коммутируют взаимно — их можно поменять местами без изменения результата.

LaTeX

$$$\\forall s\\in S,\\ A\\in (M_n(R))^{op},\\ v\\in R^n:\\ s\\cdot (A\\cdot v) = (A^{op}\\cdot (s\\cdot v))$$$

Lean4

instance [DistribSMul S R] [IsScalarTower S R R] : SMulCommClass S (Matrix n n R)ᵐᵒᵖ (n → R) where
  smul_comm s A v := (smul_vecMul s v A.unop).symm

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