Basic parity lemmas for the ring ℤ

See note [foundational algebra order theory].

Parity

theorem Int.odd_iff {n : ℤ} : Odd n ↔ n % 2 = 1

theorem Int.not_odd_iff {n : ℤ} : ¬Odd n ↔ n % 2 = 0

@[simp]

theorem Int.not_odd_zero : ¬Odd 0

@[simp]

theorem Int.not_odd_iff_even {n : ℤ} : ¬Odd n ↔ Even n

@[simp]

theorem Int.not_even_iff_odd {n : ℤ} : ¬Even n ↔ Odd n

theorem Int.even_or_odd (n : ℤ) : Even n ∨ Odd n

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

theorem Int.even_xor_odd (n : ℤ) : Xor (Even n) (Odd n)

@[deprecated Int.even_xor_odd (since := "2026-04-27")]

theorem Int.even_xor'_odd (n : ℤ) : Xor (Even n) (Odd n)

Alias of Int.even_xor_odd.

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

@[deprecated Int.even_xor_odd' (since := "2026-04-27")]

theorem Int.even_xor'_odd' (n : ℤ) : ∃ (k : ℤ), Xor (n = 2 * k) (n = 2 * k + 1)

Alias of Int.even_xor_odd'.

@[instance_reducible]

instance Int.instDecidablePredOdd : DecidablePred Odd

Equations

• x✝.instDecidablePredOdd = decidable_of_iff (¬Even x✝) ⋯

theorem Int.even_add' {m n : ℤ} : Even (m + n) ↔ (Odd m ↔ Odd n)

theorem Int.not_even_two_mul_add_one (n : ℤ) : ¬Even (2 * n + 1)

theorem Int.even_sub' {m n : ℤ} : Even (m - n) ↔ (Odd m ↔ Odd n)

theorem Int.odd_mul {m n : ℤ} : Odd (m * n) ↔ Odd m ∧ Odd n

theorem Int.Odd.of_mul_left {m n : ℤ} (h : Odd (m * n)) : Odd m

theorem Int.Odd.of_mul_right {m n : ℤ} (h : Odd (m * n)) : Odd n

theorem Int.odd_pow {m : ℤ} {n : ℕ} : Odd (m ^ n) ↔ Odd m ∨ n = 0

theorem Int.odd_pow' {m : ℤ} {n : ℕ} (h : n ≠ 0) : Odd (m ^ n) ↔ Odd m

theorem Int.odd_add {m n : ℤ} : Odd (m + n) ↔ (Odd m ↔ Even n)

theorem Int.odd_add' {m n : ℤ} : Odd (m + n) ↔ (Odd n ↔ Even m)

theorem Int.ne_of_odd_add {m n : ℤ} (h : Odd (m + n)) : m ≠ n

theorem Int.odd_sub {m n : ℤ} : Odd (m - n) ↔ (Odd m ↔ Even n)

theorem Int.odd_sub' {m n : ℤ} : Odd (m - n) ↔ (Odd n ↔ Even m)

theorem Int.even_mul_succ_self (n : ℤ) : Even (n * (n + 1))

theorem Int.even_mul_pred_self (n : ℤ) : Even (n * (n - 1))

@[simp]

theorem Int.odd_coe_nat (n : ℕ) : Odd ↑n ↔ Odd n

@[simp]

theorem Int.natAbs_even {n : ℤ} : Even n.natAbs ↔ Even n

@[simp]

theorem Int.natAbs_odd {n : ℤ} : Odd n.natAbs ↔ Odd n

theorem Even.natAbs {n : ℤ} : Even n → Even n.natAbs

Alias of the reverse direction of Int.natAbs_even.

theorem Odd.natAbs {n : ℤ} : Odd n → Odd n.natAbs

Alias of the reverse direction of Int.natAbs_odd.

theorem Int.four_dvd_add_or_sub_of_odd {a b : ℤ} (ha : Odd a) (hb : Odd b) : 4 ∣ a + b ∨ 4 ∣ a - b

theorem Int.two_dvd_mul_add_one (k : ℤ) : 2 ∣ k * (k + 1)

theorem Int.two_mul_ediv_two_add_one_of_odd {n : ℤ} : Odd n → 2 * (n / 2) + 1 = n

theorem Int.ediv_two_mul_two_add_one_of_odd {n : ℤ} : Odd n → n / 2 * 2 + 1 = n

theorem Int.add_one_ediv_two_mul_two_of_odd {n : ℤ} : Odd n → 1 + n / 2 * 2 = n

theorem Int.two_mul_ediv_two_of_odd {n : ℤ} (h : Odd n) : 2 * (n / 2) = n - 1

@[simp]

theorem Int.even_sign_iff {z : ℤ} : Even z.sign ↔ z = 0

@[simp]

theorem Int.odd_sign_iff {z : ℤ} : Odd z.sign ↔ z ≠ 0

@[simp]

theorem Int.isSquare_natCast_iff {n : ℕ} : IsSquare ↑n ↔ IsSquare n

@[simp]

theorem Int.isSquare_ofNat_iff {n : ℕ} : IsSquare (OfNat.ofNat n) ↔ IsSquare (OfNat.ofNat n)

theorem Int.natCast_pow_pred (b p : ℕ) (w : 0 < b) : ↑(b ^ p - 1) = ↑b ^ p - 1

theorem Int.coe_nat_two_pow_pred (p : ℕ) : ↑(2 ^ p - 1) = 2 ^ p - 1

theorem Int.sq_emod_four (b : ℤ) : b ^ 2 % 4 = b % 2

theorem Int.sq_emod_four_eq_one_of_odd {x : ℤ} (hx : Odd x) : x ^ 2 % 4 = 1

theorem Int.eight_dvd_sq_sub_one_of_odd {k : ℤ} (hk : Odd k) : 8 ∣ k ^ 2 - 1

theorem Odd.neg_zpow {α : Type u_1} [DivisionMonoid α] [HasDistribNeg α] {n : ℤ} (h : Odd n) (a : α) : (-a) ^ n = -a ^ n

theorem Odd.neg_one_zpow {α : Type u_1} [DivisionMonoid α] [HasDistribNeg α] {n : ℤ} (h : Odd n) : (-1) ^ n = -1