instSMulCommClassForall_1 — Mathlib

English

An alternative formulation of SMulCommClass for matrices and vectors under the same hypotheses as above, confirming commutativity of the scalar actions.

Русский

Альтернативная формулировка SMulCommClass для матриц и векторов при тех же предпосылках, подтверждающая коммутативность действий скаляров.

LaTeX

$$$\text{same as above: } s \cdot (A \cdot v) = A \cdot (s \cdot v)$$$

Lean4

instance [DistribSMul S R] [SMulCommClass S R R] : SMulCommClass S (Matrix n n R) (n → R) where
  smul_comm s A v := (mulVec_smul A s v).symm

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