mapMatrix_smul — Mathlib

English

The matrix map commutes with scalar multiplication: (a • f).mapMatrix = a • (f.mapMatrix).

Русский

Отображение матриц коммутирует с скалярным умножением: (a • f).mapMatrix = a • (f.mapMatrix).

LaTeX

$$$(a \\cdot f).mapMatrix = a \\cdot (f.mapMatrix)$$$

Lean4

@[simp]
theorem mapMatrix_smul [Monoid A] [DistribMulAction A β] [SMulCommClass S A β] (a : A) (f : α →ₛₗ[σᵣₛ] β) :
    (a • f).mapMatrix = (a • f.mapMatrix : Matrix m n α →ₛₗ[_] _) :=
  rfl

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