Theorem Function.Odd.sum_eq_zero

Modification history

2024-09-18 09:20
Mathlib/Algebra/Group/EvenFunction.lean
feat(Analysis/Fourier/ZMod): DFT preserves even/odd functions (#16911)
Added Function.Odd.sum_eq_zeroView on Github →