end_apply_apply — Mathlib

English

For any i, j, the endomorphism corresponding to (i,j) sends b_j to b_i and annihilates other basis vectors; i.e., (b.end i,j)(b k) = b_i if j = k, else 0.

Русский

Эндоморфизм, соответствующий (i,j), переводит b_j в b_i и обнуляет прочие базисные вектора; то есть (b.end i,j)(b k) = b_i, если j = k, иначе 0.

LaTeX

$$$(b.end\\, ij)(b_k) = \\begin{cases} b_i, & ij.2 = k \\\\ 0, & \\text{иначе} \\end{cases}$$$

Lean4

theorem end_apply_apply (ij : ι × ι) (k : ι) : (b.end ij) (b k) = if ij.2 = k then b ij.1 else 0 :=
  linearMap_apply_apply b b ij k

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