instSMulCommClassForall — Mathlib

English

If S distributes over R and S commutes with R, then SMulCommClass (Matrix n n R) S (n → R), i.e., the scalar action of S commutes with matrix-vector multiplication.

Русский

Если S распределительно действует над R и S коммутирует, то SMulCommClass (Matrix n n R) S (n → R), то есть действие скалярного множителя S коммутирует с умножением матрицы на вектор.

LaTeX

$$$[DistribSMul S R][SMulCommClass R S R]\Rightarrow SMulCommClass (Matrix n n R) S (n \to R)$, со свойством $s • (A • v) = A • (s • v)$ для всех $s$, $A$, $v$.$$

Lean4

instance [DistribSMul S R] [SMulCommClass R S R] : SMulCommClass (Matrix n n R) S (n → R) where
  smul_comm :=
    letI := SMulCommClass.symm;
    mulVec_smul

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