# Parity of integers #

This file contains theorems about the Even and Odd predicates on the integers.

## Tags #

even, odd

@[simp]
theorem Int.emod_two_ne_one {n : } :
¬n % 2 = 1 n % 2 = 0
@[simp]
theorem Int.one_emod_two :
1 % 2 = 1
theorem Int.emod_two_ne_zero {n : } :
¬n % 2 = 0 n % 2 = 1
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
@[simp]
theorem Int.isCompl_even_odd :
IsCompl {n : | Even n} {n : | Odd 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)
@[simp]
theorem Int.two_dvd_ne_zero {n : } :
¬2 n n % 2 = 1

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

Equations
@[simp]
theorem Int.even_add {m : } {n : } :
Even (m + n) (Even m Even n)
theorem Int.even_add' {m : } {n : } :
Even (m + n) (Odd m Odd n)
@[simp, deprecated]
theorem Int.not_even_bit1 (n : ) :
theorem Int.even_sub {m : } {n : } :
Even (m - n) (Even m Even n)
theorem Int.even_sub' {m : } {n : } :
Even (m - n) (Odd m Odd n)
theorem Int.even_add_one {n : } :
Even (n + 1) ¬Even n
theorem Int.even_sub_one {n : } :
Even (n - 1) ¬Even n
theorem Int.even_mul {m : } {n : } :
Even (m * n) Even m Even n
theorem Int.odd_mul {m : } {n : } :
Odd (m * n) Odd m Odd n
theorem Int.Odd.of_mul_left {m : } {n : } (h : Odd (m * n)) :
Odd m
theorem Int.Odd.of_mul_right {m : } {n : } (h : Odd (m * n)) :
Odd n
theorem Int.even_pow {m : } {n : } :
Even (m ^ n) Even m n 0
theorem Int.even_pow' {m : } {n : } (h : n 0) :
Even (m ^ n) Even m
theorem Int.odd_pow {m : } {n : } :
Odd (m ^ n) Odd m n = 0
theorem Int.odd_pow' {m : } {n : } (h : n 0) :
Odd (m ^ n) Odd m
theorem Int.odd_add {m : } {n : } :
Odd (m + n) (Odd m Even n)
theorem Int.odd_add' {m : } {n : } :
Odd (m + n) (Odd n Even m)
theorem Int.ne_of_odd_add {m : } {n : } (h : Odd (m + n)) :
m n
theorem Int.odd_sub {m : } {n : } :
Odd (m - n) (Odd m Even n)
theorem Int.odd_sub' {m : } {n : } :
Odd (m - n) (Odd n Even m)
theorem Int.even_mul_succ_self (n : ) :
Even (n * (n + 1))
theorem Int.even_mul_pred_self (n : ) :
Even (n * (n - 1))
@[simp]
theorem Int.even_coe_nat (n : ) :
Even n Even n
theorem Int.odd_coe_nat (n : ) :
Odd n Odd n
@[simp]
theorem Int.natAbs_even {n : } :
theorem Int.natAbs_odd {n : } :
Odd () Odd n
theorem Even.natAbs {n : } :
Even nEven ()

Alias of the reverse direction of Int.natAbs_even.

theorem Odd.natAbs {n : } :
Odd nOdd ()

Alias of the reverse direction of Int.natAbs_odd.

theorem Int.four_dvd_add_or_sub_of_odd {a : } {b : } (ha : Odd a) (hb : Odd b) :
4 a + b 4 a - b
theorem Int.two_mul_ediv_two_of_even {n : } :
Even n2 * (n / 2) = n
theorem Int.ediv_two_mul_two_of_even {n : } :
Even nn / 2 * 2 = n
theorem Int.two_mul_ediv_two_add_one_of_odd {n : } :
Odd n2 * (n / 2) + 1 = n
theorem Int.ediv_two_mul_two_add_one_of_odd {n : } :
Odd nn / 2 * 2 + 1 = n
theorem Int.add_one_ediv_two_mul_two_of_odd {n : } :
Odd n1 + n / 2 * 2 = n
theorem Int.two_mul_ediv_two_of_odd {n : } (h : Odd n) :
2 * (n / 2) = n - 1