Parity of natural numbers

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

Tags

even, odd

@[simp]

theorem Nat.mod_two_ne_one {n : ℕ} : ¬n % 2 = 1 ↔ n % 2 = 0

@[simp]

theorem Nat.mod_two_ne_zero {n : ℕ} : ¬n % 2 = 0 ↔ n % 2 = 1

theorem Nat.even_iff {n : ℕ} : Even n ↔ n % 2 = 0

instance Nat.instDecidablePredNatEvenInstAddNat : DecidablePred Even

Equations

• Nat.instDecidablePredNatEvenInstAddNat x = decidable_of_iff (x % 2 = 0) ⋯

instance Nat.instDecidablePredNatIsSquareInstMulNat : DecidablePred IsSquare

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

Equations

• Nat.instDecidablePredNatIsSquareInstMulNat m = decidable_of_iff' (Nat.sqrt m * Nat.sqrt m = m) ⋯

theorem Nat.odd_iff {n : ℕ} : Odd n ↔ n % 2 = 1

instance Nat.instDecidablePredNatOddInstSemiring : DecidablePred Odd

Equations

• Nat.instDecidablePredNatOddInstSemiring x = decidable_of_iff (x % 2 = 1) ⋯

theorem Nat.not_even_iff {n : ℕ} : ¬Even n ↔ n % 2 = 1

theorem Nat.not_odd_iff {n : ℕ} : ¬Odd n ↔ n % 2 = 0

theorem Nat.even_iff_not_odd {n : ℕ} : Even n ↔ ¬Odd n

@[simp]

theorem Nat.odd_iff_not_even {n : ℕ} : Odd n ↔ ¬Even n

theorem Odd.not_two_dvd_nat {n : ℕ} (h : Odd n) : ¬2 ∣ n

theorem Nat.isCompl_even_odd : IsCompl {n : ℕ | Even n} {n : ℕ | Odd n}

theorem Nat.even_xor_odd (n : ℕ) : Xor' (Even n) (Odd n)

theorem Nat.even_or_odd (n : ℕ) : Even n ∨ Odd n

theorem Nat.even_or_odd' (n : ℕ) : ∃ (k : ℕ), n = 2 * k ∨ n = 2 * k + 1

theorem Nat.even_xor_odd' (n : ℕ) : ∃ (k : ℕ), Xor' (n = 2 * k) (n = 2 * k + 1)

@[simp]

theorem Nat.two_dvd_ne_zero {n : ℕ} : ¬2 ∣ n ↔ n % 2 = 1

theorem Nat.mod_two_add_add_odd_mod_two (m : ℕ) {n : ℕ} (hn : Odd n) : m % 2 + (m + n) % 2 = 1

@[simp]

theorem Nat.mod_two_add_succ_mod_two (m : ℕ) : m % 2 + (m + 1) % 2 = 1

@[simp]

theorem Nat.succ_mod_two_add_mod_two (m : ℕ) : (m + 1) % 2 + m % 2 = 1

@[simp]

theorem Nat.not_even_one : ¬Even 1

theorem Nat.even_add {m : ℕ} {n : ℕ} : Even (m + n) ↔ (Even m ↔ Even n)

theorem Nat.even_add' {m : ℕ} {n : ℕ} : Even (m + n) ↔ (Odd m ↔ Odd n)

theorem Nat.even_add_one {n : ℕ} : Even (n + 1) ↔ ¬Even n

theorem Nat.succ_mod_two_eq_zero_iff {m : ℕ} : (m + 1) % 2 = 0 ↔ m % 2 = 1

theorem Nat.succ_mod_two_eq_one_iff {m : ℕ} : (m + 1) % 2 = 1 ↔ m % 2 = 0

@[simp]

theorem Nat.not_even_bit1 (n : ℕ) : ¬Even (bit1 n)

theorem Nat.two_not_dvd_two_mul_add_one (n : ℕ) : ¬2 ∣ 2 * n + 1

theorem Nat.two_not_dvd_two_mul_sub_one {n : ℕ} : 0 < n → ¬2 ∣ 2 * n - 1

theorem Nat.even_sub {m : ℕ} {n : ℕ} (h : n ≤ m) : Even (m - n) ↔ (Even m ↔ Even n)

theorem Nat.even_sub' {m : ℕ} {n : ℕ} (h : n ≤ m) : Even (m - n) ↔ (Odd m ↔ Odd n)

theorem Nat.Odd.sub_odd {m : ℕ} {n : ℕ} (hm : Odd m) (hn : Odd n) : Even (m - n)

theorem Odd.tsub_odd {m : ℕ} {n : ℕ} (hm : Odd m) (hn : Odd n) : Even (m - n)

Alias of Nat.Odd.sub_odd.

theorem Nat.even_mul {m : ℕ} {n : ℕ} : Even (m * n) ↔ Even m ∨ Even n

theorem Nat.odd_mul {m : ℕ} {n : ℕ} : Odd (m * n) ↔ Odd m ∧ Odd n

theorem Nat.Odd.of_mul_left {m : ℕ} {n : ℕ} (h : Odd (m * n)) : Odd m

theorem Nat.Odd.of_mul_right {m : ℕ} {n : ℕ} (h : Odd (m * n)) : Odd n

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.

theorem Nat.even_pow' {m : ℕ} {n : ℕ} (h : n ≠ 0) : Even (m ^ n) ↔ Even m

theorem Nat.even_div {m : ℕ} {n : ℕ} : Even (m / n) ↔ m % (2 * n) / n = 0

theorem Nat.odd_add {m : ℕ} {n : ℕ} : Odd (m + n) ↔ (Odd m ↔ Even n)

theorem Nat.odd_add' {m : ℕ} {n : ℕ} : Odd (m + n) ↔ (Odd n ↔ Even m)

theorem Nat.ne_of_odd_add {m : ℕ} {n : ℕ} (h : Odd (m + n)) : m ≠ n

theorem Nat.odd_sub {m : ℕ} {n : ℕ} (h : n ≤ m) : Odd (m - n) ↔ (Odd m ↔ Even n)

theorem Nat.Odd.sub_even {m : ℕ} {n : ℕ} (h : n ≤ m) (hm : Odd m) (hn : Even n) : Odd (m - n)

theorem Nat.odd_sub' {m : ℕ} {n : ℕ} (h : n ≤ m) : Odd (m - n) ↔ (Odd n ↔ Even m)

theorem Nat.Even.sub_odd {m : ℕ} {n : ℕ} (h : n ≤ m) (hm : Even m) (hn : Odd n) : Odd (m - n)

theorem Nat.even_mul_succ_self (n : ℕ) : Even (n * (n + 1))

theorem Nat.even_mul_pred_self (n : ℕ) : Even (n * (n - 1))

@[deprecated Nat.even_mul_pred_self]

theorem Nat.even_mul_self_pred (n : ℕ) : Even (n * (n - 1))

Alias of Nat.even_mul_pred_self.

theorem Nat.two_mul_div_two_of_even {n : ℕ} : Even n → 2 * (n / 2) = n

theorem Nat.div_two_mul_two_of_even {n : ℕ} : Even n → n / 2 * 2 = n

theorem Nat.two_mul_div_two_add_one_of_odd {n : ℕ} (h : Odd n) : 2 * (n / 2) + 1 = n

theorem Nat.div_two_mul_two_add_one_of_odd {n : ℕ} (h : Odd n) : n / 2 * 2 + 1 = n

theorem Nat.one_add_div_two_mul_two_of_odd {n : ℕ} (h : Odd n) : 1 + n / 2 * 2 = n

theorem Nat.bit0_div_two {n : ℕ} : bit0 n / 2 = n

theorem Nat.bit1_div_two {n : ℕ} : bit1 n / 2 = n

@[simp]

theorem Nat.bit0_div_bit0 {m : ℕ} {n : ℕ} : bit0 n / bit0 m = n / m

@[simp]

theorem Nat.bit1_div_bit0 {m : ℕ} {n : ℕ} : bit1 n / bit0 m = n / m

@[simp]

theorem Nat.bit0_mod_bit0 {m : ℕ} {n : ℕ} : bit0 n % bit0 m = bit0 (n % m)

@[simp]

theorem Nat.bit1_mod_bit0 {m : ℕ} {n : ℕ} : bit1 n % bit0 m = bit1 (n % m)

theorem Function.Involutive.iterate_bit0 {α : Type u_1} {f : α → α} (hf : Function.Involutive f) (n : ℕ) : f^[bit0 n] = id

theorem Function.Involutive.iterate_bit1 {α : Type u_1} {f : α → α} (hf : Function.Involutive f) (n : ℕ) : f^[bit1 n] = f

theorem Function.Involutive.iterate_two_mul {α : Type u_1} {f : α → α} (hf : Function.Involutive f) (n : ℕ) : f^[2 * n] = id

theorem Function.Involutive.iterate_even {α : Type u_1} {f : α → α} {n : ℕ} (hf : Function.Involutive f) (hn : Even n) : f^[n] = id

theorem Function.Involutive.iterate_odd {α : Type u_1} {f : α → α} {n : ℕ} (hf : Function.Involutive f) (hn : Odd n) : f^[n] = f

theorem Function.Involutive.iterate_eq_self {α : Type u_1} {f : α → α} {n : ℕ} (hf : Function.Involutive f) (hne : f ≠ id) : f^[n] = f ↔ Odd n

theorem Function.Involutive.iterate_eq_id {α : Type u_1} {f : α → α} {n : ℕ} (hf : Function.Involutive f) (hne : f ≠ id) : f^[n] = id ↔ Even n

theorem neg_one_pow_eq_one_iff_even {R : Type u_1} [Monoid R] [HasDistribNeg R] {n : ℕ} (h : -1 ≠ 1) : (-1) ^ n = 1 ↔ Even n

theorem pow_eq_pow_iff_of_ne_zero {R : Type u_1} [LinearOrderedRing R] {a : R} {b : R} {n : ℕ} (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n

theorem pow_eq_pow_iff_cases {R : Type u_1} [LinearOrderedRing R] {a : R} {b : R} {n : ℕ} : a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

theorem pow_eq_one_iff_of_ne_zero {R : Type u_1} [LinearOrderedRing R] {a : R} {n : ℕ} (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n

theorem pow_eq_one_iff_cases {R : Type u_1} [LinearOrderedRing R] {a : R} {n : ℕ} : a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n

theorem pow_eq_neg_pow_iff {R : Type u_1} [LinearOrderedRing R] {a : R} {b : R} {n : ℕ} (hb : b ≠ 0) : a ^ n = -b ^ n ↔ a = -b ∧ Odd n

theorem pow_eq_neg_one_iff {R : Type u_1} [LinearOrderedRing R] {a : R} {n : ℕ} : a ^ n = -1 ↔ a = -1 ∧ Odd n

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.

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.

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.

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.

theorem Odd.of_dvd_nat {m : ℕ} {n : ℕ} (hn : Odd n) (hm : m ∣ n) : Odd m

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.