Theorems · Definition · functional analysis
EuclideanSpace.basisFun
(ι : Type u_1) → (𝕜 : Type u_3) → [inst : RCLike 𝕜] → [inst_1 : Fintype ι] → OrthonormalBasis ι 𝕜 (EuclideanSpace 𝕜 ι)
The basis Pi.basisFun, bundled as an orthonormal basis of EuclideanSpace 𝕜 ι.
- Defined in
- Mathlib.Analysis.InnerProductSpace.PiL2
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 227 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement · cited by 9,879
- Fintypestatement and proof · cited by 7,736
- RCLikestatement and proof · cited by 2,829
- EuclideanSpacestatement and proof · cited by 307
- OrthonormalBasisstatement · cited by 188
- LinearIsometryEquiv.reflproof · cited by 23
Cited by29
Results whose statement or proof uses this declaration.
- Matrix.IsHermitian.eigenvectorUnitaryproof · cited by 25
- Matrix.toEuclideanCLMproof · cited by 12
- EuclideanSpace.basisFun_innerstatement and proof · cited by 5
- EuclideanSpace.volume_preserving_symm_measurableEquiv_toLpproof · cited by 4
- EuclideanSpace.basisFun_applystatement · cited by 4
- Matrix.isSymmetric_toEuclideanLin_iffproof · cited by 3
- ProbabilityTheory.covariance_eval_multivariateGaussianproof · cited by 3
- Matrix.toEuclideanLin_eq_toLin_orthonormalstatement · cited by 2
- NumberField.mixedEmbedding.euclidean.stdOrthonormalBasisproof · cited by 2
- OrthonormalBasis.measurePreserving_measurableEquivproof · cited by 2
- ProbabilityTheory.covarianceBilin_apply_basisFunstatement and proof · cited by 1
- ProbabilityTheory.covarianceBilin_apply_piproof · cited by 1