Zulip Chat Archive

Stream: new members

Topic: even not odd


view this post on Zulip 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?

view this post on Zulip Jalex Stark (Feb 26 2020 at 16:26):

Look at data.nat.parity

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Feb 26 2020 at 17:08):

There's nat.mod_two_eq_zero_or_one

view this post on Zulip 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