smulCommClass — Mathlib

English

The scalar action commutes with matrix multiplication on both sides: (r • A) B = A (r • B) for all r ∈ R and A, B in Mn×n(α).

Русский

Действие скаляра коммутирует с умножением матриц слева и справа: (r • A) B = A (r • B).

LaTeX

$$$ (r \\cdot A) \\cdot B = A \\cdot (r \\cdot B) $$$

Lean4

/-- This instance enables use with `mul_smul_comm`. -/
instance smulCommClass [Fintype n] [Monoid R] [DistribMulAction R α] [SMulCommClass R α α] :
    SMulCommClass R (Matrix n n α) (Matrix n n α) :=
  ⟨fun r m n => (Matrix.mul_smul m r n).symm⟩

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