mathlib3 documentation

data.zmod.parity

Relating parity to natural numbers mod 2 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This module provides lemmas relating zmod 2 to even and odd.

Tags #

parity, zmod, even, odd

source
theorem zmod.eq_zero_iff_even {n : ℕ} :
↑n = 0 ↔ even n
source
theorem zmod.eq_one_iff_odd {n : ℕ} :
↑n = 1 ↔ odd n
source
theorem zmod.ne_zero_iff_odd {n : ℕ} :
↑n ≠ 0 ↔ odd n