mathlib documentation

data.zmod.parity

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