Theorems · Inductive type · functional analysis

OrthonormalBasis

(ι : Type u_1) →
  (𝕜 : Type u_3) →
    [inst : RCLike 𝕜] →
      (E : Type u_4) →
        [inst_1 : NormedAddCommGroup E] → [InnerProductSpace 𝕜 E] → [Fintype ι] → Type (max (max u_1 u_3) u_4)

An orthonormal basis on E is an identification of E with its dimensional-matching EuclideanSpace 𝕜 ι.

Defined in

Mathlib.Analysis.InnerProductSpace.PiL2

Cited by

188 results in Mathlib

Foundations

Depth 11 from the axioms, rests on 69 definitions · uses no axioms

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceFintype