Relating parity to natural numbers mod 2

This module provides lemmas relating ZMod 2 to Even and Odd.

Tags

parity, zmod, even, odd

theorem ZMod.eq_zero_iff_even {n : ℕ} : ↑n = 0 ↔ Even n

theorem ZMod.eq_one_iff_odd {n : ℕ} : ↑n = 1 ↔ Odd n

theorem ZMod.ne_zero_iff_odd {n : ℕ} : ↑n ≠ 0 ↔ Odd n