Theorems · Theorem · functional analysis
WithLp.linearEquiv_symm_apply
∀ (p : ENNReal) (K : Type u_1) (V : Type u_4) [inst : Semiring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (a : V), (WithLp.linearEquiv p K V).symm a = (WithLp.addEquiv p V).invFun a
- Defined in
- Mathlib.Analysis.Normed.Lp.WithLp
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemiringAddCommGroupModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- AddCommGroupstatement and proof · cited by 12,871
- ENNRealstatement and proof · cited by 9,879
- LinearEquivstatement · cited by 3,317
- LinearEquiv.symmstatement and proof · cited by 1,461
- WithLpstatement · cited by 345
- AddEquiv.toEquivstatement · cited by 174
- Equiv.invFunstatement · cited by 163
- WithLp.linearEquivstatement and proof · cited by 29
Cited by11
Results whose statement or proof uses this declaration.
- Submodule.orthogonalDecomposition_applyproof · cited by 6
- LinearIsometryEquiv.piLpCongrLeft_symmproof · cited by 2
- LinearMap.posSemidef_toMatrix_iffproof · cited by 1
- OrthonormalBasis.sum_repr_symmproof · cited by 1
- InnerProductSpace.symm_toEuclideanLin_rankOneproof · cited by 1
- OrthonormalBasis.tensorProduct_repr_tmul_applyproof · cited by 1
- PiLp.basis_toMatrix_basisFun_mulproof · cited by 0
- PiLp.linearIndependent_singleproof · cited by 0
- PiLp.linearIndependent_single_of_ne_zeroproof · cited by 0
- PiLp.linearIndependent_single_oneproof · cited by 0
- OrthonormalBasis.prod_applyproof · cited by 0