Commit 2020-10-02 13:06 2ce359b9

feat(data/nat/parity,data/int/parity): odd numbers (#4357) As discussed at https://leanprover.zulipchat.com/#narrow/stream/208328-IMO-grand-challenge/topic/formalizing.20IMO.20problems, define nat.odd and int.odd to allow a more literal expression (outside of mathlib; for example, in formal olympiad problem statements) of results whose informal statement refers to odd numbers. These definitions are not expected to be used in mathlib beyond the simp lemmas added here that translate them back to ¬ even. This is similar to how > is defined but almost all mathlib results are expected to use < instead. It's likely that expressing olympiad problem statements literally in Lean will end up using some other such definitions, where avoiding API duplication means almost everything relevant in mathlib is developed in terms of the expansion of the definition.