instIsScalarTowerMulOppositeForallOfSMulCommClass

English

The tower condition holds for the actions of S on MulOpposite(Matrix n n R) and on vectors: s • (Aᵒᵖ • v) = (s • A)ᵒᵖ • v for all s, A, v.

Русский

Условия башни выполняются для действий S на MulOpposite(Матрица) и на вектора: 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] [SMulCommClass S R R] : IsScalarTower S (Matrix n n R)ᵐᵒᵖ (n → R) where
  smul_assoc s A v := vecMul_smul v s A.unop

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