dualBasis_repr_apply — Mathlib

English

For x in V and i in ι, the i-th coordinate of x with respect to the B-dual basis equals B(x, b_i).

Русский

Для x∈V и i∈ι i-я координата по B-двойственной базе равна B(x, b_i).

LaTeX

$$$\\big( (B.dualBasis hB b).repr\\;x \\big)(i) = B\\,x\\,(b_i).$$$

Lean4

@[simp]
theorem dualBasis_repr_apply (B : BilinForm K V) (hB : B.Nondegenerate) (b : Basis ι K V) (x i) :
    (B.dualBasis hB b).repr x i = B x (b i) :=
  by
  have := FiniteDimensional.of_fintype_basis b
  rw [dualBasis, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply, Basis.dualBasis_repr, toDual_def]

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