coe_toOrthonormalBasis_repr — Mathlib

English

The coefficient mapping of a basis to an orthonormal basis respects the representation of vectors.

Русский

Коэффициентное отображение базиса в ортонормированный базис сохраняет представление векторов.

LaTeX

$$$((v.toOrthonormalBasis hv).repr : E → EuclideanSpace 𝕜 ι) = v.equivFun$$$

Lean4

@[simp]
theorem _root_.Module.Basis.coe_toOrthonormalBasis_repr (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) :
    ((v.toOrthonormalBasis hv).repr : E → EuclideanSpace 𝕜 ι) = v.equivFun :=
  rfl

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