apply_dualBasis_right — Mathlib

English

If B is symmetric, then B(b_i, dualBasis_j) = δ_{ij}. This follows from the left version by symmetry.

Русский

Если B симметрична, то B(b_i, dualBasis_j) = δ_{ij}. Это следует из левой версии симметрией.

LaTeX

$$$B\\big(b_i, B.dualBasis hB b j\\big) = \\delta_{ij} = \\begin{cases}1,& i=j,\\\\ 0,& i\\neq j.\\end{cases}$$$

Lean4

theorem apply_dualBasis_right (B : BilinForm K V) (hB : B.Nondegenerate) (sym : B.IsSymm) (b : Basis ι K V) (i j) :
    B (b i) (B.dualBasis hB b j) = if i = j then 1 else 0 := by rw [sym.eq, apply_dualBasis_left]

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