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

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