norm_eq_one — Mathlib

English

The action of b on the i-th coordinate vector matches the i-th vector of the basis under the repr correspondence.

Русский

Действие базиса на i-й вектор координат совпадает с i-й векторной базисной по отображению через repr.

LaTeX

$$b.repr (b i) = EuclideanSpace.single i (1 : 𝕜)$$

Lean4

@[simp]
theorem norm_eq_one (b : OrthonormalBasis ι 𝕜 E) (i : ι) : ‖b i‖ = 1 :=
  b.orthonormal.norm_eq_one i

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