Commit 2024-09-13 06:50 0fc9f199

View on Github →

feat(Algebra/Group): define even and odd functions (#16446) Define predicates Function.Even and Function.Odd for functions satisfying f (-x) = f x resp. f (-x) = -(f x), and prove some simple properties of these.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Group/EvenFunction.lean

added theorem Function.Even.add

added theorem Function.Even.comp_odd

added theorem Function.Even.const

added theorem Function.Even.const_smul

added theorem Function.Even.left_comp

added theorem Function.Even.mul_even

added theorem Function.Even.mul_odd

added theorem Function.Even.smul_even

added theorem Function.Even.smul_odd

added theorem Function.Even.zero

added theorem Function.Odd.add

added theorem Function.Odd.comp_odd

added theorem Function.Odd.const_smul

added theorem Function.Odd.mul_even

added theorem Function.Odd.mul_odd

added theorem Function.Odd.smul_even

added theorem Function.Odd.smul_odd

added theorem Function.Odd.zero

added theorem Function.zero_of_even_and_odd