repr_self — Mathlib

English

For an orthonormal basis b, and any vector v, the i-th coordinate of v in the basis equals the inner product of b i with v.

Русский

Для ортонормированного базиса b коэффициент координат вектору v по индексу i равен скалярному произведению b i с v.

LaTeX

$$b.repr v i = ⟪b i, v⟫$$

Lean4

@[simp]
protected theorem repr_self [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) :
    b.repr (b i) = EuclideanSpace.single i (1 : 𝕜) := by
  rw [← b.repr_symm_single i, LinearIsometryEquiv.apply_symm_apply]

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