mathlib documentation

data.nat.parity

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
def nat.even (n : ℕ) :
Prop

A natural number n is even if 2 | n.

Equations
source
theorem nat.even_iff {n : ℕ} :
n.even ↔ n % 2 = 0

source
theorem nat.not_even_iff {n : ℕ} :
¬n.even ↔ n % 2 = 1

source
@[instance]
def nat.decidable_pred  :
decidable_pred nat.even

Equations
source
@[simp]
theorem nat.even_zero  :
0.even

source
@[simp]
theorem nat.not_even_one  :
¬1.even

source
@[simp]
theorem nat.even_bit0 (n : ℕ) :
(bit0 n).even

source
theorem nat.even_add {m n : ℕ} :
(m + n).even ↔ (m.even ↔ n.even)

source
theorem nat.even.add {m n : ℕ} (hm : m.even) (hn : n.even) :
(m + n).even

source
@[simp]
theorem nat.not_even_bit1 (n : ℕ) :
¬(bit1 n).even

source
theorem nat.two_not_dvd_two_mul_add_one (a : ℕ) :
¬2 ∣ 2 * a + 1

source
theorem nat.two_not_dvd_two_mul_sub_one {a : ℕ} (w : 0 < a) :
¬2 ∣ 2 * a - 1

source
theorem nat.even_sub {m n : ℕ} (h : n ≤ m) :
(m - n).even ↔ (m.even ↔ n.even)

source
theorem nat.even.sub {m n : ℕ} (hm : m.even) (hn : n.even) :
(m - n).even

source
theorem nat.even_succ {n : ℕ} :
n.succ.even ↔ ¬n.even

source
theorem nat.even_mul {m n : ℕ} :
(m * n).even ↔ m.even ∨ n.even

source
theorem nat.even_pow {m n : ℕ} :
(m ^ n).even ↔ m.even ∧ 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_div {a b : ℕ} :
(a / b).even ↔ a % 2 * b / b = 0

source
theorem nat.neg_one_pow_eq_one_iff_even {α : Type u_1} [ring α] {n : ℕ} (h1 : -1 ≠ 1) :
(-1) ^ n = 1 ↔ n.even