even/odd functions

Stream: new members

[Callum Cassidy-Nolan]

I was looking through https://leanprover-community.github.io/mathlib_docs_demo/init/function.html for the definition of even/odd function, do these definitions exist in mathlib?

[Jireh Loreaux]

I haven't seen it (which doesn't mean it isn't there!), but if we did have it, then the appropriate level of generality would be something like an involutive linear map on a module over a ring of characteristic different from 2. Any such map decomposes the module into a fixed part, and an anti-fixed part. For even functions (the fixed part) the involution is (lambda x, f x) -> (lambda x, f -x). (Sorry, on mobile)

[Kevin Buzzard]

For the definition you would only need your domain to have a - for even and for the codomain also to have one for odd. To statethe theorem that every function is even+odd you would need an addition and to prove it you'd need an action of the integers on the codomain and the fact that 2 acts invertibly (eg it could be a module for a ring in which is_unit 2)

[Kevin Buzzard]

We have add_hom; an odd function is neg_hom.