instSMulCommClassMulOppositeForallOfIsScalarTower

English

The scalar actions from S and from the opposite matrix algebra on column vectors commute. In particular, for s ∈ S, A ∈ (M_n(R))^op, v ∈ R^n, we have s · (A · v) = (s · A) · v.

Русский

Скалярные действия из S и из противоположной матричной алгебры на столбцовых векторах коммютативны: s · (A · v) = (s · A) · v.

LaTeX

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

Lean4

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

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