isScalarTower — Mathlib

English

This instance asserts the compatibility of scalar multiplication with matrix multiplication: for all r in R and matrices M, N, (r • M) · N = r • (M · N).

Русский

Это свойство совместимости скаляра с умножением матриц: для всех r в R и матриц M, N выполняется (r • M) · N = r • (M · N).

LaTeX

$$$ (r \\cdot M) \\cdot N = r \\cdot (M \\cdot N) $$$

Lean4

/-- This instance enables use with `smul_mul_assoc`. -/
instance isScalarTower [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α] :
    IsScalarTower R (Matrix n n α) (Matrix n n α) :=
  ⟨fun r m n => Matrix.smul_mul r m n⟩

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