## Stream: new members

### Topic: even not odd

#### Alex Kontorovich (Feb 26 2020 at 16:25):

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

#### Jalex Stark (Feb 26 2020 at 16:26):

Look at data.nat.parity

#### Kevin Buzzard (Feb 26 2020 at 17:04):

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 (Feb 26 2020 at 17:08):

There's nat.mod_two_eq_zero_or_one

#### Kevin Buzzard (Feb 26 2020 at 17:09):

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

Last updated: May 08 2021 at 09:11 UTC