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

theorem Int.even_iff_not_odd {n : ℤ} : Even n ↔ ¬Odd n

@[simp]

theorem Int.odd_iff_not_even {n : ℤ} : Odd n ↔ ¬Even n

theorem Int.isCompl_even_odd : IsCompl {n : ℤ | Even n} {n : ℤ | Odd n}

theorem Int.even_or_odd (n : ℤ) : Even n ∨ 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

instance Int.instDecidablePredIntEvenInstAddInt : DecidablePred Even

Equations

• Int.instDecidablePredIntEvenInstAddInt x = decidable_of_iff (x % 2 = 0) ⋯

instance Int.instDecidablePredIntOddInstSemiring : DecidablePred Odd

Equations

• Int.instDecidablePredIntOddInstSemiring x = decidable_of_iff (¬Even x) ⋯

instance Int.instDecidablePredIntIsSquareInstMulInt : DecidablePred IsSquare

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

Equations

• Int.instDecidablePredIntIsSquareInstMulInt m = decidable_of_iff' (Int.sqrt m * Int.sqrt m = m) ⋯

@[simp]

theorem Int.not_even_one : ¬Even 1

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 : ℤ) : ¬Even (bit1 n)

theorem Int.two_not_dvd_two_mul_add_one (n : ℤ) : ¬2 ∣ 2 * n + 1

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 : ℤ} : Even (Int.natAbs n) ↔ Even n

theorem Int.natAbs_odd {n : ℤ} : Odd (Int.natAbs n) ↔ Odd n

theorem Even.natAbs {n : ℤ} : Even n → Even (Int.natAbs n)

Alias of the reverse direction of Int.natAbs_even.

theorem Odd.natAbs {n : ℤ} : Odd n → Odd (Int.natAbs n)

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 n → 2 * (n / 2) = n

theorem Int.ediv_two_mul_two_of_even {n : ℤ} : Even n → n / 2 * 2 = n

theorem Int.two_mul_ediv_two_add_one_of_odd {n : ℤ} : Odd n → 2 * (n / 2) + 1 = n

theorem Int.ediv_two_mul_two_add_one_of_odd {n : ℤ} : Odd n → n / 2 * 2 + 1 = n

theorem Int.add_one_ediv_two_mul_two_of_odd {n : ℤ} : Odd n → 1 + n / 2 * 2 = n

theorem Int.two_mul_ediv_two_of_odd {n : ℤ} (h : Odd n) : 2 * (n / 2) = n - 1