# `IsSquare` and `Even` for natural numbers #

#### Parity #

source
theorem Nat.even_iff {n : ℕ} :
Even n ↔ n % 2 = 0
source
instance Nat.instDecidablePredEven :
DecidablePred Even
Equations

- x✝.instDecidablePredEven = decidable_of_iff (x✝ % 2 = 0) ⋯

source
instance Nat.instDecidablePredIsSquare :
DecidablePred IsSquare

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

Equations

- m.instDecidablePredIsSquare = decidable_of_iff' (m.sqrt * m.sqrt = m) ⋯

source
theorem Nat.not_even_iff {n : ℕ} :
¬Even n ↔ n % 2 = 1
source
@[simp]
theorem Nat.two_dvd_ne_zero {n : ℕ} :
¬2 ∣ n ↔ n % 2 = 1
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_one {n : ℕ} :
Even (n + 1) ↔ ¬Even n
source
theorem Nat.succ_mod_two_eq_zero_iff {m : ℕ} :
(m + 1) % 2 = 0 ↔ m % 2 = 1
source
theorem Nat.succ_mod_two_eq_one_iff {m : ℕ} :
(m + 1) % 2 = 1 ↔ m % 2 = 0
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 : ℕ} :
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_mul {m n : ℕ} :
Even (m * n) ↔ Even m ∨ Even 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_mul_succ_self (n : ℕ) :
Even (n * (n + 1))
source
theorem Nat.even_mul_pred_self (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.one_lt_of_ne_zero_of_even {n : ℕ} (h0 : n ≠ 0) (hn : Even n) :
1 < n
source
theorem Nat.add_one_lt_of_even {m n : ℕ} (hn : Even n) (hm : Even m) (hnm : n < m) :
n + 1 < m