scilib documentation

data.nat.parity

Parity of natural numbers #

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 natural numbers.

Tags #

even, odd

source
@[simp]
theorem nat.mod_two_ne_one {n : ℕ} :
¬n % 2 = 1 ↔ n % 2 = 0
source
@[simp]
theorem nat.mod_two_ne_zero {n : ℕ} :
¬n % 2 = 0 ↔ n % 2 = 1
source
theorem nat.even_iff {n : ℕ} :
even n ↔ n % 2 = 0
source
theorem nat.odd_iff {n : ℕ} :
odd n ↔ n % 2 = 1
source
theorem nat.not_even_iff {n : ℕ} :
¬even n ↔ n % 2 = 1
source
theorem nat.not_odd_iff {n : ℕ} :
¬odd n ↔ n % 2 = 0
source
theorem nat.even_iff_not_odd {n : ℕ} :
even n ↔ ¬odd n
source
@[simp]
theorem nat.odd_iff_not_even {n : ℕ} :
odd n ↔ ¬even n
source
theorem nat.is_compl_even_odd  :
is_compl {n : ℕ | even n} {n : ℕ | odd n}
source
theorem nat.even_or_odd (n : ℕ) :
even n ∨ odd n
source
theorem nat.even_or_odd' (n : ℕ) :
∃ (k : ℕ), n = 2 * k ∨ n = 2 * k + 1
source
theorem nat.even_xor_odd (n : ℕ) :
xor (even n) (odd n)
source
theorem nat.even_xor_odd' (n : ℕ) :
∃ (k : ℕ), xor (n = 2 * k) (n = 2 * k + 1)
source
@[simp]
theorem nat.two_dvd_ne_zero {n : ℕ} :
¬2 ∣ n ↔ n % 2 = 1
source
@[protected, instance]
def nat.even.decidable_pred  :
decidable_pred even
Equations
source
@[protected, instance]
def nat.odd.decidable_pred  :
decidable_pred odd
Equations
source
theorem nat.mod_two_add_add_odd_mod_two (m : ℕ) {n : ℕ} (hn : odd n) :
m % 2 + (m + n) % 2 = 1
source
@[simp]
theorem nat.mod_two_add_succ_mod_two (m : ℕ) :
m % 2 + (m + 1) % 2 = 1
source
@[simp]
theorem nat.succ_mod_two_add_mod_two (m : ℕ) :
(m + 1) % 2 + m % 2 = 1
source
meta def simp_attr.parity_simps  :
(user_attribute simp_lemmas)

Simp attribute for lemmas about even

source
@[simp]
theorem nat.not_even_one  :
¬even 1
source
theorem nat.even_add {m n : ℕ} :
even (m + n) ↔ (even m ↔ even n)
source
theorem nat.even_add' {m n : ℕ} :
even (m + n) ↔ (odd m ↔ odd n)
source
theorem nat.even_add_one {n : ℕ} :
even (n + 1) ↔ ¬even n
source
@[simp]
theorem nat.not_even_bit1 (n : ℕ) :
¬even (bit1 n)
source
theorem nat.two_not_dvd_two_mul_add_one (n : ℕ) :
¬2 ∣ 2 * n + 1
source
theorem nat.two_not_dvd_two_mul_sub_one {n : ℕ} (w : 0 < n) :
¬2 ∣ 2 * n - 1
source
theorem nat.even_sub {m n : ℕ} (h : n ≤ m) :
even (m - n) ↔ (even m ↔ even n)
source
theorem nat.even_sub' {m n : ℕ} (h : n ≤ m) :
even (m - n) ↔ (odd m ↔ odd n)
source
theorem nat.odd.sub_odd {m n : ℕ} (hm : odd m) (hn : odd n) :
even (m - n)
source
theorem nat.even_mul {m n : ℕ} :
even (m * n) ↔ even m ∨ even n
source
theorem nat.odd_mul {m n : ℕ} :
odd (m * n) ↔ odd m ∧ odd n
source
theorem nat.odd.of_mul_left {m n : ℕ} (h : odd (m * n)) :
odd m
source
theorem nat.odd.of_mul_right {m n : ℕ} (h : odd (m * n)) :
odd n
source
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.

source
theorem nat.even_pow' {m n : ℕ} (h : n ≠ 0) :
even (m ^ n) ↔ even m
source
theorem nat.even_div {m n : ℕ} :
even (m / n) ↔ m % (2 * n) / n = 0
source
theorem nat.odd_add {m n : ℕ} :
odd (m + n) ↔ (odd m ↔ even n)
source
theorem nat.odd_add' {m n : ℕ} :
odd (m + n) ↔ (odd n ↔ even m)
source
theorem nat.ne_of_odd_add {m n : ℕ} (h : odd (m + n)) :
m ≠ n
source
theorem nat.odd_sub {m n : ℕ} (h : n ≤ m) :
odd (m - n) ↔ (odd m ↔ even n)
source
theorem nat.odd.sub_even {m n : ℕ} (h : n ≤ m) (hm : odd m) (hn : even n) :
odd (m - n)
source
theorem nat.odd_sub' {m n : ℕ} (h : n ≤ m) :
odd (m - n) ↔ (odd n ↔ even m)
source
theorem nat.even.sub_odd {m n : ℕ} (h : n ≤ m) (hm : even m) (hn : odd n) :
odd (m - n)
source
theorem nat.even_mul_succ_self (n : ℕ) :
even (n * (n + 1))
source
theorem nat.even_mul_self_pred (n : ℕ) :
even (n * (n - 1))
source
theorem nat.two_mul_div_two_of_even {n : ℕ} :
even n → 2 * (n / 2) = n
source
theorem nat.div_two_mul_two_of_even {n : ℕ} :
even n → n / 2 * 2 = n
source
theorem nat.two_mul_div_two_add_one_of_odd {n : ℕ} (h : odd n) :
2 * (n / 2) + 1 = n
source
theorem nat.div_two_mul_two_add_one_of_odd {n : ℕ} (h : odd n) :
n / 2 * 2 + 1 = n
source
theorem nat.one_add_div_two_mul_two_of_odd {n : ℕ} (h : odd n) :
1 + n / 2 * 2 = n
source
theorem nat.bit0_div_two {n : ℕ} :
bit0 n / 2 = n
source
theorem nat.bit1_div_two {n : ℕ} :
bit1 n / 2 = n
source
@[simp]
theorem nat.bit0_div_bit0 {m n : ℕ} :
bit0 n / bit0 m = n / m
source
@[simp]
theorem nat.bit1_div_bit0 {m n : ℕ} :
bit1 n / bit0 m = n / m
source
@[simp]
theorem nat.bit0_mod_bit0 {m n : ℕ} :
bit0 n % bit0 m = bit0 (n % m)
source
@[simp]
theorem nat.bit1_mod_bit0 {m n : ℕ} :
bit1 n % bit0 m = bit1 (n % m)
source
theorem function.involutive.iterate_bit0 {α : Type u_1} {f : α → α} (hf : function.involutive f) (n : ℕ) :
f^[bit0 n] = id
source
theorem function.involutive.iterate_bit1 {α : Type u_1} {f : α → α} (hf : function.involutive f) (n : ℕ) :
f^[bit1 n] = f
source
theorem function.involutive.iterate_even {α : Type u_1} {f : α → α} {n : ℕ} (hf : function.involutive f) (hn : even n) :
f^[n] = id
source
theorem function.involutive.iterate_odd {α : Type u_1} {f : α → α} {n : ℕ} (hf : function.involutive f) (hn : odd n) :
f^[n] = f
source
theorem function.involutive.iterate_eq_self {α : Type u_1} {f : α → α} {n : ℕ} (hf : function.involutive f) (hne : f ≠ id) :
f^[n] = f ↔ odd n
source
theorem function.involutive.iterate_eq_id {α : Type u_1} {f : α → α} {n : ℕ} (hf : function.involutive f) (hne : f ≠ id) :
f^[n] = id ↔ even n
source
theorem neg_one_pow_eq_one_iff_even {R : Type u_1} [monoid R] [has_distrib_neg R] {n : ℕ} (h : -1 ≠ 1) :
(-1) ^ n = 1 ↔ even n
source
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.

source
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.

source
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.

source
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.

source
theorem odd.of_dvd_nat {m n : ℕ} (hn : odd n) (hm : m ∣ n) :
odd m
source
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.