mapMatrix_comp — Mathlib

English

The identity linear map maps matrices to themselves: id.mapMatrix is the identity on matrix spaces.

Русский

Тождественное линейное отображение отображает матрицы в самих себя: id.mapMatrix — тождество на пространствах матриц.

LaTeX

$$$\\mathrm{LinearMap.id}.\\mathrm{mapMatrix} = \\mathrm{LinearMap.id}$$$

Lean4

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

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