mathlib documentation

data.nat.parity

Parity of natural numbers #

This file contains theorems about the even and odd predicates on the natural numbers.

Tags #

even, odd

@[simp]
theorem nat.mod_two_ne_one {n : } :
¬n % 2 = 1 n % 2 = 0
@[simp]
theorem nat.mod_two_ne_zero {n : } :
¬n % 2 = 0 n % 2 = 1
theorem nat.even_iff {n : } :
even n n % 2 = 0
theorem nat.odd_iff {n : } :
odd n n % 2 = 1
theorem nat.not_even_iff {n : } :
¬even n n % 2 = 1
theorem nat.not_odd_iff {n : } :
¬odd n n % 2 = 0
theorem nat.even_iff_not_odd {n : } :
@[simp]
theorem nat.odd_iff_not_even {n : } :
theorem nat.is_compl_even_odd  :
is_compl {n : | even n} {n : | odd n}
theorem nat.even_or_odd (n : ) :
theorem nat.even_or_odd' (n : ) :
∃ (k : ), n = 2 * k n = 2 * k + 1
theorem nat.even_xor_odd (n : ) :
xor (even n) (odd n)
theorem nat.even_xor_odd' (n : ) :
∃ (k : ), xor (n = 2 * k) (n = 2 * k + 1)
theorem nat.odd_gt_zero {n : } (h : odd n) :
0 < n
@[simp]
theorem nat.two_dvd_ne_zero {n : } :
¬2 n n % 2 = 1

Simp attribute for lemmas about even

@[simp]
theorem nat.even_zero  :
@[simp]
theorem nat.not_even_one  :
@[simp]
theorem nat.even_bit0 (n : ) :
theorem nat.even_add {m n : } :
even (m + n) (even m even n)
theorem nat.even.add_even {m n : } (hm : even m) (hn : even n) :
even (m + n)
theorem nat.even_add' {m n : } :
even (m + n) (odd m odd n)
theorem nat.odd.add_odd {m n : } (hm : odd m) (hn : odd n) :
even (m + n)
@[simp]
theorem nat.not_even_bit1 (n : ) :
theorem nat.two_not_dvd_two_mul_add_one (n : ) :
¬2 2 * n + 1
theorem nat.two_not_dvd_two_mul_sub_one {n : } (w : 0 < n) :
¬2 2 * n - 1
theorem nat.even_sub {m n : } (h : n m) :
even (m - n) (even m even n)
theorem nat.even.sub_even {m n : } (hm : even m) (hn : even n) :
even (m - n)
theorem nat.even_sub' {m n : } (h : n m) :
even (m - n) (odd m odd n)
theorem nat.odd.sub_odd {m n : } (hm : odd m) (hn : odd n) :
even (m - n)
theorem nat.even_succ {n : } :
theorem nat.even_mul {m n : } :
even (m * n) even m even n
theorem nat.odd_mul {m n : } :
odd (m * n) odd m odd n
theorem nat.even.mul_left {m : } (hm : even m) (n : ) :
even (m * n)
theorem nat.even.mul_right {n : } (m : ) (hn : even n) :
even (m * n)
theorem nat.odd.mul {m n : } (hm : odd m) (hn : odd n) :
odd (m * n)
theorem nat.odd.of_mul_left {m n : } (h : odd (m * n)) :
odd m
theorem nat.odd.of_mul_right {m n : } (h : odd (m * n)) :
odd n
theorem nat.even_pow {m n : } :
even (m ^ n) even m n 0

If m and n are natural numbers, then the natural number m^n is even if and only if m is even and n is positive.

theorem nat.even_pow' {m n : } (h : n 0) :
even (m ^ n) even m
theorem nat.even_div {m n : } :
even (m / n) m % 2 * n / n = 0
theorem nat.odd_add {m n : } :
odd (m + n) (odd m even n)
theorem nat.odd.add_even {m n : } (hm : odd m) (hn : even n) :
odd (m + n)
theorem nat.odd_add' {m n : } :
odd (m + n) (odd n even m)
theorem nat.even.add_odd {m n : } (hm : even m) (hn : odd n) :
odd (m + n)
theorem nat.ne_of_odd_add {m n : } (h : odd (m + n)) :
m n
theorem nat.odd_sub {m n : } (h : n m) :
odd (m - n) (odd m even n)
theorem nat.odd.sub_even {m n : } (h : n m) (hm : odd m) (hn : even n) :
odd (m - n)
theorem nat.odd_sub' {m n : } (h : n m) :
odd (m - n) (odd n even m)
theorem nat.even.sub_odd {m n : } (h : n m) (hm : even m) (hn : odd n) :
odd (m - n)
theorem nat.even_mul_succ_self (n : ) :
even (n * (n + 1))
theorem nat.neg_one_pow_eq_one_iff_even {n : } {R : Type u_1} [ring R] (h1 : -1 1) :
(-1) ^ n = 1 even n
@[simp]
theorem nat.neg_one_sq {R : Type u_1} [ring R] :
(-1) ^ 2 = 1
theorem nat.neg_one_pow_two {R : Type u_1} [ring R] :
(-1) ^ 2 = 1

Alias of nat.neg_one_sq.

theorem nat.neg_one_pow_of_even {n : } {R : Type u_1} [ring R] :
even n(-1) ^ n = 1
theorem nat.neg_one_pow_of_odd {n : } {R : Type u_1} [ring R] :
odd n(-1) ^ n = -1