mk_coord_apply_ne — Mathlib

English

If j ≠ i, the i-th dual coordinate evaluated at v_j is 0.

Русский

Если j ≠ i, то i-й двойственный координат, применённый к v_j, равен 0.

LaTeX

$$$\\text{if } j \\neq i:\\; (Basis.mk hli hsp).coord\\ i\\ (v_j) = 0$$$

Lean4

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

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