mathlib3 documentation

data.int.parity

Parity of integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Tags #

even, odd

source
@[simp]
theorem int.mod_two_ne_one {n : ℤ} :
¬n % 2 = 1 ↔ n % 2 = 0
source
theorem int.mod_two_ne_zero {n : ℤ} :
¬n % 2 = 0 ↔ n % 2 = 1
source
theorem int.even_iff {n : ℤ} :
even n ↔ n % 2 = 0
source
theorem int.odd_iff {n : ℤ} :
odd n ↔ n % 2 = 1
source
theorem int.not_even_iff {n : ℤ} :
¬even n ↔ n % 2 = 1
source
theorem int.not_odd_iff {n : ℤ} :
¬odd n ↔ n % 2 = 0
source
theorem int.even_iff_not_odd {n : ℤ} :
even n ↔ ¬odd n
source
@[simp]
theorem int.odd_iff_not_even {n : ℤ} :
odd n ↔ ¬even n
source
theorem int.is_compl_even_odd  :
is_compl {n : ℤ | even n} {n : ℤ | odd n}
source
theorem int.even_or_odd (n : ℤ) :
even n ∨ odd n
source
theorem int.even_or_odd' (n : ℤ) :
∃ (k : ℤ), n = 2 * k ∨ n = 2 * k + 1
source
theorem int.even_xor_odd (n : ℤ) :
xor (even n) (odd n)
source
theorem int.even_xor_odd' (n : ℤ) :
∃ (k : ℤ), xor (n = 2 * k) (n = 2 * k + 1)
source
@[simp]
theorem int.two_dvd_ne_zero {n : ℤ} :
¬2 ∣ n ↔ n % 2 = 1
source
@[protected, instance]
def int.even.decidable_pred  :
decidable_pred even
Equations
source
@[protected, instance]
def int.odd.decidable_pred  :
decidable_pred odd
Equations
source
@[simp]
theorem int.not_even_one  :
¬even 1
source
theorem int.even_add {m n : ℤ} :
even (m + n) ↔ (even m ↔ even n)
source
theorem int.even_add' {m n : ℤ} :
even (m + n) ↔ (odd m ↔ odd n)
source
@[simp]
theorem int.not_even_bit1 (n : ℤ) :
¬even (bit1 n)
source
theorem int.two_not_dvd_two_mul_add_one (n : ℤ) :
¬2 ∣ 2 * n + 1
source
theorem int.even_sub {m n : ℤ} :
even (m - n) ↔ (even m ↔ even n)
source
theorem int.even_sub' {m n : ℤ} :
even (m - n) ↔ (odd m ↔ odd n)
source
theorem int.even_add_one {n : ℤ} :
even (n + 1) ↔ ¬even n
source
theorem int.even_mul {m n : ℤ} :
even (m * n) ↔ even m ∨ even n
source
theorem int.odd_mul {m n : ℤ} :
odd (m * n) ↔ odd m ∧ odd n
source
theorem int.odd.of_mul_left {m n : ℤ} (h : odd (m * n)) :
odd m
source
theorem int.odd.of_mul_right {m n : ℤ} (h : odd (m * n)) :
odd n
source
theorem int.even_pow {m : ℤ} {n : ℕ} :
even (m ^ n) ↔ even m ∧ n ≠ 0
source
theorem int.even_pow' {m : ℤ} {n : ℕ} (h : n ≠ 0) :
even (m ^ n) ↔ even m
source
theorem int.odd_add {m n : ℤ} :
odd (m + n) ↔ (odd m ↔ even n)
source
theorem int.odd_add' {m n : ℤ} :
odd (m + n) ↔ (odd n ↔ even m)
source
theorem int.ne_of_odd_add {m n : ℤ} (h : odd (m + n)) :
m ≠ n
source
theorem int.odd_sub {m n : ℤ} :
odd (m - n) ↔ (odd m ↔ even n)
source
theorem int.odd_sub' {m n : ℤ} :
odd (m - n) ↔ (odd n ↔ even m)
source
theorem int.even_mul_succ_self (n : ℤ) :
even (n * (n + 1))
source
@[simp, norm_cast]
theorem int.even_coe_nat (n : ℕ) :
even ↑n ↔ even n
source
@[simp, norm_cast]
theorem int.odd_coe_nat (n : ℕ) :
odd ↑n ↔ odd n
source
@[simp]
theorem int.nat_abs_even {n : ℤ} :
even n.nat_abs ↔ even n
source
@[simp]
theorem int.nat_abs_odd {n : ℤ} :
odd n.nat_abs ↔ odd n
source
@[protected]
theorem even.nat_abs {n : ℤ} :
even n → even n.nat_abs

Alias of the reverse direction of int.nat_abs_even.

source
@[protected]
theorem odd.nat_abs {n : ℤ} :
odd n → odd n.nat_abs

Alias of the reverse direction of int.nat_abs_odd.

source
theorem int.four_dvd_add_or_sub_of_odd {a b : ℤ} (ha : odd a) (hb : odd b) :
4 ∣ a + b ∨ 4 ∣ a - b
source
theorem int.two_mul_div_two_of_even {n : ℤ} :
even n → 2 * (n / 2) = n
source
theorem int.div_two_mul_two_of_even {n : ℤ} :
even n → n / 2 * 2 = n
source
theorem int.two_mul_div_two_add_one_of_odd {n : ℤ} :
odd n → 2 * (n / 2) + 1 = n
source
theorem int.div_two_mul_two_add_one_of_odd {n : ℤ} :
odd n → n / 2 * 2 + 1 = n
source
theorem int.add_one_div_two_mul_two_of_odd {n : ℤ} :
odd n → 1 + n / 2 * 2 = n
source
theorem int.two_mul_div_two_of_odd {n : ℤ} (h : odd n) :
2 * (n / 2) = n - 1