mathlib documentation

data.int.parity

@[simp]
theorem int.mod_two_ne_one {n : } :
¬n % 2 = 1 n % 2 = 0

theorem int.mod_two_ne_zero {n : } :
¬n % 2 = 0 n % 2 = 1

@[simp]
theorem int.even_coe_nat (n : ) :

theorem int.even_iff {n : } :
even n n % 2 = 0

theorem int.odd_iff {n : } :
odd n n % 2 = 1

theorem int.not_even_iff {n : } :
¬even n n % 2 = 1

theorem int.not_odd_iff {n : } :
¬odd n n % 2 = 0

theorem int.even_iff_not_odd {n : } :

@[simp]
theorem int.odd_iff_not_even {n : } :

theorem int.even_or_odd (n : ) :

theorem int.even_or_odd' (n : ) :
∃ (k : ), n = 2 * k n = 2 * k + 1

theorem int.even_xor_odd (n : ) :
xor (even n) (odd n)

theorem int.even_xor_odd' (n : ) :
∃ (k : ), xor (n = 2 * k) (n = 2 * k + 1)

theorem int.ne_of_odd_sum {x y : } (h : odd (x + y)) :
x y

@[simp]
theorem int.two_dvd_ne_zero {n : } :
¬2 n n % 2 = 1

@[simp]
theorem int.even_zero  :

@[simp]
theorem int.not_even_one  :

@[simp]
theorem int.even_bit0 (n : ) :

theorem int.even_add {m n : } :
even (m + n) (even m even n)

theorem int.even_neg {n : } :
even (-n) even n

@[simp]
theorem int.not_even_bit1 (n : ) :

theorem int.even_sub {m n : } :
even (m - n) (even m even n)

theorem int.even_mul {m n : } :
even (m * n) even m even n

theorem int.even_pow {m : } {n : } :
even (m ^ n) even m n 0