linearMap_apply_apply — Mathlib

English

For the i,j-th basis map L_{i,j}, applying to b1(k) yields b2(i) if j = k, and 0 otherwise.

Русский

У отображения L_{i,j} на вектор b1(k) получается b2(i) если j = k, иначе 0.

LaTeX

$$$(b_1.linearMap b_2)_{(i,j)}(b_1(k)) = \\begin{cases} b_2(i), & j = k \\\\ 0, & \\text{otherwise} \\end{cases}$$$

Lean4

theorem linearMap_apply_apply (ij : ι₂ × ι₁) (k : ι₁) : (b₁.linearMap b₂ ij) (b₁ k) = if ij.2 = k then b₂ ij.1 else 0 :=
  by
  have := Classical.decEq ι₂
  rw [linearMap_apply, Matrix.stdBasis_eq_single, Matrix.toLin_self]
  dsimp only [Matrix.single, of_apply]
  simp_rw [ite_smul, one_smul, zero_smul, ite_and, Finset.sum_ite_eq, Finset.mem_univ, if_true]

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