even not odd

Stream: new members

[Alex Kontorovich]

Very stupid question: does mathlib have something that knows that a natural number is even or odd but not both?

[Jalex Stark]

Look at data.nat.parity

[Kevin Buzzard]

This file only defines even, it does not define odd. If one were to define odd as "not even" then Alex's question becomes very easy! On the other hand a lemma in the file says that n is even iff n % 2 = 0 and other lemmas show that n % 2 is always exactly one of 0 or 1, so one could define odd as n % 2 = 1 and then the lemmas do everything you need.

[Chris Hughes]

There's nat.mod_two_eq_zero_or_one

[Kevin Buzzard]

aah, this is hidden away in data.int.basic