linearMap_apply — Mathlib

English

The i,j-th basis map in the standard basis of Hom(M1,M2) equals the linear map corresponding to the standard matrix unit under the chosen bases, i.e., (b1.linearMap b2)_{i,j} equals Matrix.toLin b1 b2 applied to the standard basis E_{ij}.

Русский

Элемент базы линейного отображения, соответствующий индексу (i, j), равен линейному отображению, получаемому из матричного единичного элемента по выбранным базисам: (b1.linearMap b2)_{i,j} = Matrix.toLin b1 b2 (E_{ij}).

LaTeX

$$$ (b_1.linearMap b_2)_{(i,j)} = (\\mathrm{Matrix}.toLin\\,b_1\\,b_2)(E_{ij})$$$

Lean4

theorem linearMap_apply (ij : ι₂ × ι₁) : (b₁.linearMap b₂ ij) = (Matrix.toLin b₁ b₂) (Matrix.stdBasis R ι₂ ι₁ ij) := by
  simp [linearMap]

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