mathlib
bb2b58ed - feat(data/{nat,int}/parity): add division lemmas (#11570)

Commit
4 years ago
feat(data/{nat,int}/parity): add division lemmas (#11570) Add lemmas of the form `even n → n / 2 * 2 = n` and `odd n → n / 2 * 2 + 1 = n`
Author
Parents
Loading