Theorem Function.Odd.map_zero

Modification history

2025-10-17 16:01
Mathlib/Algebra/Group/EvenFunction.lean
chore(Algebra/Group/EvenFunction): don't import torsion-free modules (#30628) …
Modified Function.Odd.map_zeroView on Github →
2024-09-18 09:20
Mathlib/Algebra/Group/EvenFunction.lean
feat(Analysis/Fourier/ZMod): DFT preserves even/odd functions (#16911)
Added Function.Odd.map_zeroView on Github →