Theorem Real.Lp.coe_fourierTransform

Modification history

2026-03-10 22:48
Mathlib/Analysis/Fourier/FourierTransform.lean
feat(Analysis/Fourier): the Fourier transform as bounded continuous function (#35954) …
Added Real.Lp.coe_fourierTransformView on Github →