Theorems · Definition · functional analysis
OrthonormalBasis.repr
{ι : Type u_1} →
{𝕜 : Type u_3} →
[inst : RCLike 𝕜] →
{E : Type u_4} →
[inst_1 : NormedAddCommGroup E] →
[inst_2 : InnerProductSpace 𝕜 E] → [inst_3 : Fintype ι] → OrthonormalBasis ι 𝕜 E → E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ιLinear isometry between E and EuclideanSpace 𝕜 ι representing the orthonormal basis.
- Defined in
- Mathlib.Analysis.InnerProductSpace.PiL2
- Cited by
- 61 results in Mathlib
- Foundations
- Depth 221 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHom.idstatement · cited by 18,349
- NormedAddCommGroupstatement and proof · cited by 15,752
- ENNRealstatement · cited by 9,879
- Fintypestatement and proof · cited by 7,736
- InnerProductSpacestatement and proof · cited by 3,523
- RCLikestatement and proof · cited by 2,829
- LinearIsometryEquivstatement · cited by 748
- EuclideanSpacestatement · cited by 307
- OrthonormalBasisstatement and proof · cited by 188
Cited by70
Results whose statement or proof uses this declaration.
- OrthonormalBasis.toBasisproof · cited by 102
- OrthonormalBasis.reindexproof · cited by 15
- OrthonormalBasis.orthonormalproof · cited by 14
- OrthonormalBasis.repr_apply_applystatement and proof · cited by 11
- OrthonormalBasis.mapproof · cited by 10
- OrthonormalBasis.coe_toBasis_repr_applystatement and proof · cited by 8
- OrthonormalBasis.equivproof · cited by 8
- OrthonormalBasis.sum_reprstatement and proof · cited by 7
- stereographic'proof · cited by 5
- OrthonormalBasis.repr_selfstatement and proof · cited by 4
- OrthonormalBasis.measurePreserving_repr_symmstatement · cited by 4
- OrthonormalBasis.reindex_applyproof · cited by 3