Theorems · Theorem
FourierTransform.fourierEquiv_symm_apply
∀ {R : Type u_5} {E : Type u_6} {F : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
[inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : FourierTransform E F] [inst_6 : FourierAdd E F]
[inst_7 : FourierSMul R E F] [inst_8 : FourierTransformInv F E] [inst_9 : FourierPair E F]
[inst_10 : FourierInvPair F E] (f : F), (FourierTransform.fourierEquiv R E).symm f = FourierTransformInv.fourierInv f- Defined in
- Mathlib.Analysis.Fourier.Notation
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- LinearEquivstatement · cited by 3,317
- LinearEquiv.symmstatement · cited by 1,461
- FourierTransformInv.fourierInvstatement · cited by 69
- FourierTransformInvstatement and proof · cited by 25
- FourierTransformstatement and proof · cited by 23
- FourierAddstatement and proof · cited by 14
- FourierSMulstatement and proof · cited by 11
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.