mapMatrix_sub — Mathlib

English

The matrix map respects subtraction: (f - g).mapMatrix equals f.mapMatrix minus g.mapMatrix.

Русский

Отображение по матрицам сохраняет вычитание: (f - g).mapMatrix = f.mapMatrix - g.mapMatrix.

LaTeX

$$$ (f - g).mapMatrix = (f.mapMatrix - g.mapMatrix) $$$

Lean4

@[simp]
theorem mapMatrix_sub (f g : α →ₛₗ[σᵣₛ] β) :
    (f - g).mapMatrix = (f.mapMatrix - g.mapMatrix : Matrix m n α →ₛₗ[σᵣₛ] _) :=
  rfl

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