toDual_apply — Mathlib

English

For any i and j in the index set ι, the value of the dual map on a pair of basis vectors is the Kronecker delta: b.toDual(b_i)(b_j) = δ_{ij}.

Русский

Для любых индексов i, j из множества индексов ι значение дуального отображения на пару базисных векторов равно кронекерову дельте: b.toDual(b_i)(b_j) = δ_{ij}.

LaTeX

$$$ b.toDual (b_i)(b_j) = \delta_{ij}. $$$

Lean4

theorem toDual_apply (i j : ι) : b.toDual (b i) (b j) = if i = j then 1 else 0 :=
  by
  rw [toDual, constr_basis b, constr_basis b]
  simp only [eq_comm]

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