mk_coord_apply_eq — Mathlib

English

The i-th element of the dual basis evaluates to 1 on the i-th basis vector.

Русский

i-й элемент двойственной базы оценивается как 1 на i-м элементе базиса.

LaTeX

$$$(Basis.mk hli hsp).coord\\ i\\ (v_i) = 1$$$

Lean4

/-- Given a basis, the `i`th element of the dual basis evaluates to 1 on the `i`th element of the
basis. -/
theorem mk_coord_apply_eq (i : ι) : (Basis.mk hli hsp).coord i (v i) = 1 :=
  show hli.repr ⟨v i, Submodule.subset_span (mem_range_self i)⟩ i = 1 by simp [hli.repr_eq_single i]

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