smul_mul — Mathlib

English

For a scalar a and matrices M,N, (a • M) * N = a • (M * N).

Русский

Для скаляра a и матриц M,N выполняется (a • M) · N = a • (M · N).

LaTeX

$$$ (a \cdot M) * N = a \cdot (M * N) $$$

Lean4

@[simp]
theorem smul_mul {l : Type*} [Fintype n] [Monoid R] [AddCommMonoid A] [Mul A] [DistribMulAction R A]
    [IsScalarTower R A A] (a : R) (M : CStarMatrix m n A) (N : CStarMatrix n l A) : (a • M) * N = a • (M * N) :=
  Matrix.smul_mul a M N

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