repr_symm_single — Mathlib

English

The i-th coordinate of the representation equals the inner product ⟪b_i, v⟫.

Русский

i-я координата представления равна скалярному произведению ⟪b_i, v⟫.

LaTeX

$$$ \\text{repr } v(i) = \\langle b_i, v \\rangle $$$

Lean4

@[simp]
protected theorem repr_symm_single [DecidableEq ι] (b : HilbertBasis ι 𝕜 E) (i : ι) :
    b.repr.symm (lp.single 2 i (1 : 𝕜)) = b i := by
  dsimp [instFunLike]
  convert rfl

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