Commit 2026-01-27 22:28 ed96f50f

View on Github →

feat(Analysis/Fourier): simp lemmas for 0 and neg (#34285)

Estimated changes

Modified Mathlib/Analysis/Fourier/Notation.lean

added theorem FourierTransform.fourierInv_neg

added theorem FourierTransform.fourierInv_sum

modified theorem FourierTransform.fourierInv_zero

added theorem FourierTransform.fourier_neg

added theorem FourierTransform.fourier_sum

modified theorem FourierTransform.fourier_zero