coe_toDual_self — Mathlib

English

For each i, the dual vector corresponding to the basis vector b_i is the i-th coordinate functional, i.e., b.toDual(b_i) = b.coord(i).

Русский

Для каждого i дуальный вектор, соответствующий базисному вектору b_i, является i-й координатной функциональной, то есть b.toDual(b_i) = b.coord(i).

LaTeX

$$$ b.toDual (b i) = b.coord i. $$$

Lean4

theorem coe_toDual_self (i : ι) : b.toDual (b i) = b.coord i :=
  by
  ext
  apply toDual_apply_right

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