Commit 2024-09-18 09:20 36a333ac

View on Github →

feat(Analysis/Fourier/ZMod): DFT preserves even/odd functions (#16911)

Estimated changes

Modified Mathlib/Algebra/Group/EvenFunction.lean

added theorem Function.Odd.map_zero

added theorem Function.Odd.sum_eq_zero

modified theorem Function.zero_of_even_and_odd

Modified Mathlib/Analysis/Fourier/ZMod.lean

added theorem ZMod.dft_even_iff

added theorem ZMod.dft_odd_iff