Theorems · Definition · functional analysis

InnerProductSpace.gramSchmidt

(𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [InnerProductSpace 𝕜 E] →
          {ι : Type u_3} → [inst : LinearOrder ι] → [LocallyFiniteOrderBot ι] → [WellFoundedLT ι] → (ι → E) → ι → E

The Gram-Schmidt process takes a set of vectors as input and outputs a set of orthogonal vectors which have the same span.

Defined in

Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Cited by

30 results in Mathlib

Foundations

Depth 181 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceLinearOrderLocallyFiniteOrderBotWellFoundedLT