Theorems · Definition · Lie groups
Real.fourierChar
AddChar ℝ Circle
The additive character from ℝ onto the circle, given by fun x ↦ exp (2 * π * x * I).
Denoted as 𝐞 within the Real.FourierTransform namespace. This uses the analyst convention that
there is a 2 * π in the exponent.
- Defined in
- Mathlib.Analysis.Complex.Circle
- Cited by
- 59 results in Mathlib
- Foundations
- Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Realstatement and proof · cited by 25,697
- Real.piproof · cited by 1,774
- AddCharstatement · cited by 286
- Circlestatement · cited by 227
- Circle.expproof · cited by 73
Cited by59
Results whose statement or proof uses this declaration.
- Real.continuous_fourierCharstatement · cited by 10
- Real.fourierIntegral_continuousLinearMap_apply'statement · cited by 5
- VectorFourier.hasFDerivAt_fourierIntegralstatement and proof · cited by 5
- Real.fourierInv_eq_fourier_negproof · cited by 4
- VectorFourier.contDiff_fourierIntegralstatement and proof · cited by 4
- Real.hasDerivAt_fourierCharstatement and proof · cited by 4
- MeasureTheory.charFun_eq_fourierIntegral'statement and proof · cited by 3
- Real.fourierIntegral_continuousMultilinearMap_apply'statement · cited by 3
- Real.fourierIntegral_convergent_iffstatement · cited by 3
- Real.fourierInv_eqstatement and proof · cited by 3
- Real.fourier_bilin_convolution_eqproof · cited by 3
- VectorFourier.iteratedFDeriv_fourierIntegralstatement · cited by 3