Theorems · Theorem · Lie groups
Real.continuous_fourierChar
Continuous ⇑Real.fourierChar
- Defined in
- Mathlib.Analysis.Complex.Circle
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 173 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Realstatement · cited by 25,697
- Continuousstatement · cited by 2,592
- Real.piproof · cited by 1,774
- Continuous.compproof · cited by 371
- AddCharstatement · cited by 286
- Circlestatement · cited by 227
- ContinuousMap.continuousproof · cited by 74
- Circle.expproof · cited by 73
- Real.fourierCharstatement · cited by 59
- continuous_const_mulproof · cited by 47
Cited by10
Results whose statement or proof uses this declaration.
- Real.fourierIntegral_continuousLinearMap_apply'proof · cited by 5
- VectorFourier.hasFDerivAt_fourierIntegralproof · cited by 5
- SchwartzMap.integral_bilin_fourier_eqproof · cited by 3
- Real.fourierIntegral_continuousMultilinearMap_apply'proof · cited by 3
- Real.fourierIntegral_convergent_iff'proof · cited by 2
- Real.fourier_bilin_convolution_eq_integralproof · cited by 1
- Real.tendsto_integral_gaussian_smulproof · cited by 1
- SchwartzMap.integral_sesq_fourier_eqproof · cited by 1
- MeasureTheory.iteratedFDeriv_charFunproof · cited by 1
- VectorFourier.hasFTaylorSeriesUpTo_fourierIntegralproof · cited by 1