apply_dualBasis_left — Mathlib

English

For a nondegenerate B and B.isSymm, the i-th dual basis vector paired with b_j yields δ_{ji}. In particular, B(dualBasis_i, b_j) = δ_{ji}.

Русский

Для невырожденной B и симметричной B, i-й вектор двойственной базы, взятый с базисом b, образует δ_{ji} при скоблении с b_j.

LaTeX

$$$B\\left(B.dualBasis hB b i\\,,\\; b_j\\right) = \\delta_{ji} = \\begin{cases}1,& j=i,\\\\ 0,& j\\neq i.\\end{cases}$$$

Lean4

theorem apply_dualBasis_left (B : BilinForm K V) (hB : B.Nondegenerate) (b : Basis ι K V) (i j) :
    B (B.dualBasis hB b i) (b j) = if j = i then 1 else 0 :=
  by
  have := FiniteDimensional.of_fintype_basis b
  rw [dualBasis, Basis.map_apply, Basis.coe_dualBasis, ← toDual_def hB, LinearEquiv.apply_symm_apply, Basis.coord_apply,
    Basis.repr_self, Finsupp.single_apply]

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