mathlib documentation

data.nat.parity

@[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

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

theorem nat.odd_gt_zero {n : } :
odd n0 < n

@[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 {m n : } :
even meven neven (m + n)

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

theorem nat.two_not_dvd_two_mul_add_one (a : ) :
¬2 2 * a + 1

theorem nat.two_not_dvd_two_mul_sub_one {a : } :
0 < a¬2 2 * a - 1

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

theorem nat.even.sub {m n : } :
even meven neven (m - n)

theorem nat.even_succ {n : } :

theorem nat.even_mul {m n : } :
even (m * n) even m even 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_div {a b : } :
even (a / b) a % 2 * b / b = 0

theorem nat.neg_one_pow_eq_one_iff_even {α : Type u_1} [ring α] {n : } :
-1 1((-1) ^ n = 1 even n)