# 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

IsSquare can be decided on ℕ by checking against the square root.

Equations
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
@[simp]
theorem Odd.not_two_dvd_nat {n : } (h : Odd n) :
¬2 n
theorem Nat.isCompl_even_odd :
IsCompl {n : | Even n} {n : | Odd n}
theorem Nat.even_xor_odd (n : ) :
Xor' (Even 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 : ) :
∃ (k : ), Xor' (n = 2 * k) (n = 2 * k + 1)
@[simp]
theorem Nat.two_dvd_ne_zero {n : } :
¬2 n n % 2 = 1
theorem Nat.mod_two_add_add_odd_mod_two (m : ) {n : } (hn : Odd n) :
m % 2 + (m + n) % 2 = 1
@[simp]
theorem Nat.mod_two_add_succ_mod_two (m : ) :
m % 2 + (m + 1) % 2 = 1
@[simp]
theorem Nat.succ_mod_two_add_mod_two (m : ) :
(m + 1) % 2 + m % 2 = 1
@[simp]
theorem Nat.even_add {m : } {n : } :
Even (m + n) (Even m Even n)
theorem Nat.even_add' {m : } {n : } :
Even (m + n) (Odd m Odd n)
theorem Nat.even_add_one {n : } :
Even (n + 1) ¬Even n
theorem Nat.succ_mod_two_eq_zero_iff {m : } :
(m + 1) % 2 = 0 m % 2 = 1
theorem Nat.succ_mod_two_eq_one_iff {m : } :
(m + 1) % 2 = 1 m % 2 = 0
@[simp]
theorem Nat.not_even_bit1 (n : ) :
theorem Nat.two_not_dvd_two_mul_sub_one {n : } :
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' {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 Odd.tsub_odd {m : } {n : } (hm : Odd m) (hn : Odd n) :
Even (m - n)

Alias of Nat.Odd.sub_odd.

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.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' {m : } {n : } :
Odd (m + n) (Odd n Even m)
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.even_mul_pred_self (n : ) :
Even (n * (n - 1))
@[deprecated Nat.even_mul_pred_self]
theorem Nat.even_mul_self_pred (n : ) :
Even (n * (n - 1))

Alias of Nat.even_mul_pred_self.

theorem Nat.two_mul_div_two_of_even {n : } :
Even n2 * (n / 2) = n
theorem Nat.div_two_mul_two_of_even {n : } :
Even nn / 2 * 2 = n
theorem Nat.two_mul_div_two_add_one_of_odd {n : } (h : Odd n) :
2 * (n / 2) + 1 = n
theorem Nat.div_two_mul_two_add_one_of_odd {n : } (h : Odd n) :
n / 2 * 2 + 1 = n
theorem Nat.one_add_div_two_mul_two_of_odd {n : } (h : Odd n) :
1 + n / 2 * 2 = n
theorem Nat.bit0_div_two {n : } :
bit0 n / 2 = n
theorem Nat.bit1_div_two {n : } :
bit1 n / 2 = n
@[simp]
theorem Nat.bit0_div_bit0 {m : } {n : } :
bit0 n / bit0 m = n / m
@[simp]
theorem Nat.bit1_div_bit0 {m : } {n : } :
bit1 n / bit0 m = n / m
@[simp]
theorem Nat.bit0_mod_bit0 {m : } {n : } :
bit0 n % bit0 m = bit0 (n % m)
@[simp]
theorem Nat.bit1_mod_bit0 {m : } {n : } :
bit1 n % bit0 m = bit1 (n % m)
theorem Function.Involutive.iterate_bit0 {α : Type u_1} {f : αα} (hf : ) (n : ) :
f^[bit0 n] = id
theorem Function.Involutive.iterate_bit1 {α : Type u_1} {f : αα} (hf : ) (n : ) :
f^[bit1 n] = f
theorem Function.Involutive.iterate_two_mul {α : Type u_1} {f : αα} (hf : ) (n : ) :
f^[2 * n] = id
theorem Function.Involutive.iterate_even {α : Type u_1} {f : αα} {n : } (hf : ) (hn : Even n) :
f^[n] = id
theorem Function.Involutive.iterate_odd {α : Type u_1} {f : αα} {n : } (hf : ) (hn : Odd n) :
f^[n] = f
theorem Function.Involutive.iterate_eq_self {α : Type u_1} {f : αα} {n : } (hf : ) (hne : f id) :
f^[n] = f Odd n
theorem Function.Involutive.iterate_eq_id {α : Type u_1} {f : αα} {n : } (hf : ) (hne : f id) :
f^[n] = id Even n
theorem neg_one_pow_eq_one_iff_even {R : Type u_1} [] [] {n : } (h : -1 1) :
(-1) ^ n = 1 Even n
theorem pow_eq_pow_iff_of_ne_zero {R : Type u_1} {a : R} {b : R} {n : } (hn : n 0) :
a ^ n = b ^ n a = b a = -b Even n
theorem pow_eq_pow_iff_cases {R : Type u_1} {a : R} {b : R} {n : } :
a ^ n = b ^ n n = 0 a = b a = -b Even n
theorem pow_eq_one_iff_of_ne_zero {R : Type u_1} {a : R} {n : } (hn : n 0) :
a ^ n = 1 a = 1 a = -1 Even n
theorem pow_eq_one_iff_cases {R : Type u_1} {a : R} {n : } :
a ^ n = 1 n = 0 a = 1 a = -1 Even n
theorem pow_eq_neg_pow_iff {R : Type u_1} {a : R} {b : R} {n : } (hb : b 0) :
a ^ n = -b ^ n a = -b Odd n
theorem pow_eq_neg_one_iff {R : Type u_1} {a : R} {n : } :
a ^ n = -1 a = -1 Odd n
theorem Odd.mod_even_iff {n : } {a : } (ha : Even a) :
Odd (n % a) Odd n

If a is even, then n is odd iff n % a is odd.

theorem Even.mod_even_iff {n : } {a : } (ha : Even a) :
Even (n % a) Even n

If a is even, then n is even iff n % a is even.

theorem Odd.mod_even {n : } {a : } (hn : Odd n) (ha : Even a) :
Odd (n % a)

If n is odd and a is even, then n % a is odd.

theorem Even.mod_even {n : } {a : } (hn : Even n) (ha : Even a) :
Even (n % a)

If n is even and a is even, then n % a is even.

theorem Odd.of_dvd_nat {m : } {n : } (hn : Odd n) (hm : m n) :
Odd m
theorem Odd.ne_two_of_dvd_nat {m : } {n : } (hn : Odd n) (hm : m n) :
m 2

2 is not a factor of an odd natural number.