mk_coord_apply — Mathlib

English

The dual coordinate evaluates to the Kronecker delta: it is 1 when j = i and 0 otherwise.

Русский

Двойная координата дает дельта Кронекера: 1, если j = i, иначе 0.

LaTeX

$$$(Basis.mk hli hsp).coord\\ i\\ (v\\ j) = \\begin{cases}1,& j=i\\\\0,& j\\neq i\\end{cases}$$$

Lean4

/-- Given a basis, the `i`th element of the dual basis evaluates to the Kronecker delta on the
`j`th element of the basis. -/
theorem mk_coord_apply [DecidableEq ι] {i j : ι} : (Basis.mk hli hsp).coord i (v j) = if j = i then 1 else 0 :=
  by
  rcases eq_or_ne j i with h | h
  · simp only [h, if_true, mk_coord_apply_eq i]
  · simp only [h, if_false, mk_coord_apply_ne h]

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