IsSquare and Even for natural numbers

Parity

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

@[implicit_reducible]

instance Nat.instDecidablePredEven : DecidablePred Even

@[implicit_reducible]

instance Nat.instDecidablePredIsSquare : DecidablePred IsSquare

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

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

@[simp]

theorem Nat.two_dvd_ne_zero {n : ℕ} : ¬2 ∣ n ↔ n % 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_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

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_mul {m n : ℕ} : Even (m * n) ↔ Even m ∨ Even 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_mul_succ_self (n : ℕ) : Even (n * (n + 1))

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

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.one_lt_of_ne_zero_of_even {n : ℕ} (h0 : n ≠ 0) (hn : Even n) : 1 < n

theorem Nat.add_one_lt_of_even {m n : ℕ} (hn : Even n) (hm : Even m) (hnm : n < m) : n + 1 < m