Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC