Mathlib Map

Theorems · Definition · functional analysis

InnerProductSpace.gramSchmidtNormed

(𝕜 : 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 normalized gramSchmidt (i.e each vector in gramSchmidtNormed has unit length.)

Defined in
Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Cited by
13 results in Mathlib
Foundations
Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
RCLikeNormedAddCommGroupInnerProductSpaceLinearOrderLocallyFiniteOrderBotWellFoundedLT
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

InnerProductSpace.gramSchmidtOrthonormalBasis_apply · cited by 3InnerProductSpace.gramSch…InnerProductSpace.span_gramSchmidtNormed · cited by 2InnerProductSpace.span_gr…InnerProductSpace.inner_gramSchmidtOrthonormalBasis_eq_zero · cited by 1InnerProductSpace.inner_g…InnerProductSpace.gramSchmidtNormed_orthonormal' · cited by 1InnerProductSpace.gramSch…InnerProductSpace.gramSchmidtNormed_unit_length · cited by 1InnerProductSpace.gramSch…InnerProductSpace.gramSchmidtNormed_unit_length' · cited by 1InnerProductSpace.gramSch…InnerProductSpace.gramSchmidtNormed_unit_length_coe · cited by 1InnerProductSpace.gramSch…InnerProductSpace.gramSchmidtOrthonormalBasis_apply_of_orthogonal · cited by 1InnerProductSpace.gramSch…InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular · cited by 1InnerProductSpace.gramSch…InnerProductSpace.span_gramSchmidtNormed_range · cited by 0InnerProductSpace.span_gr…InnerProductSpace.gramSchmidtNormed_linearIndependent · cited by 0InnerProductSpace.gramSch…InnerProductSpace.gramSchmidtNormed_orthonormal · cited by 0InnerProductSpace.gramSch…InnerProductSpace.gramSchmidtNormed.congr_simp · cited by 0gramSchmidtNormed.congr_s…NormedAddCommGroup · cited by 15752NormedAddCommGroupLinearOrder · cited by 8572LinearOrderNorm.norm · cited by 5413Norm.normInnerProductSpace · cited by 3523InnerProductSpaceRCLike · cited by 2829RCLikeWellFoundedLT · cited by 491WellFoundedLTRCLike.ofReal · cited by 350RCLike.ofRealLocallyFiniteOrderBot · cited by 286LocallyFiniteOrderBotInnerProductSpace.gramSchmidt · cited by 30InnerProductSpace.gramSch…InnerProductSpace.gramSchmidt…CITED BYCITES

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by13

Results whose statement or proof uses this declaration.