Theorems · Definition · functional analysis
PiLp.basisFun
(p : ENNReal) → (𝕜 : Type u_1) → (ι : Type u_2) → [Finite ι] → [inst : Ring 𝕜] → Module.Basis ι 𝕜 (PiLp p fun x => 𝕜)
A version of Pi.basisFun for PiLp.
- Defined in
- Mathlib.Analysis.Normed.Lp.PiLp
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement and proof · cited by 9,879
- Ringstatement and proof · cited by 7,463
- Finitestatement and proof · cited by 3,029
- Module.Basisstatement · cited by 1,477
- PiLpstatement · cited by 150
- WithLp.linearEquivproof · cited by 29
- Module.Basis.ofEquivFunproof · cited by 7
Cited by12
Results whose statement or proof uses this declaration.
- Matrix.spectrum_toLpLinproof · cited by 2
- PiLp.basisFun_applystatement · cited by 1
- PiLp.basisFun_eq_pi_basisFunstatement · cited by 0
- PiLp.basisFun_equivFunstatement · cited by 0
- PiLp.basisFun_mapstatement · cited by 0
- PiLp.basisFun_reprstatement · cited by 0
- PiLp.basis_toMatrix_basisFun_mulstatement and proof · cited by 0
- Matrix.toEuclideanLin_eq_toLinstatement · cited by 0
- EuclideanSpace.basisFun_toBasisstatement · cited by 0
- Matrix.toLpLin_eq_toLinstatement · cited by 0
- PiLp.basisFun.congr_simpstatement and proof · cited by 0
- LinearMap.det_toLpLinproof · cited by 0