Documentation

Mathlib.Algebra.Ring.Int.Parity

Basic parity lemmas for the ring ℤ #

See note [foundational algebra order theory].

Parity #

source
theorem Int.odd_iff {n : ℤ} :
Odd n ↔ n % 2 = 1
source
theorem Int.not_odd_iff {n : ℤ} :
¬Odd n ↔ n % 2 = 0
source
@[simp]
theorem Int.not_odd_zero :
¬Odd 0
source
@[simp]
theorem Int.not_odd_iff_even {n : ℤ} :
¬Odd n ↔ Even n
source
@[simp]
theorem Int.not_even_iff_odd {n : ℤ} :
¬Even n ↔ Odd n
source
theorem Int.even_or_odd (n : ℤ) :
Even n ∨ Odd n
source
theorem Int.even_or_odd' (n : ℤ) :
∃ (k : ℤ), n = 2 * k ∨ n = 2 * k + 1
source
theorem Int.even_xor_odd (n : ℤ) :
Xor (Even n) (Odd n)
source
@[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.

source
theorem Int.even_xor_odd' (n : ℤ) :
∃ (k : ℤ), Xor (n = 2 * k) (n = 2 * k + 1)
source
@[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'.

source
@[implicit_reducible]
instance Int.instDecidablePredOdd :
DecidablePred Odd
Equations
source
theorem Int.even_add' {m n : ℤ} :
Even (m + n) ↔ (Odd m ↔ Odd n)
source
theorem Int.not_even_two_mul_add_one (n : ℤ) :
¬Even (2 * n + 1)
source
theorem Int.even_sub' {m n : ℤ} :
Even (m - n) ↔ (Odd m ↔ Odd n)
source
theorem Int.odd_mul {m n : ℤ} :
Odd (m * n) ↔ Odd m ∧ Odd n
source
theorem Int.Odd.of_mul_left {m n : ℤ} (h : Odd (m * n)) :
Odd m
source
theorem Int.Odd.of_mul_right {m n : ℤ} (h : Odd (m * n)) :
Odd n
source
theorem Int.odd_pow {m : ℤ} {n : ℕ} :
Odd (m ^ n) ↔ Odd m ∨ n = 0
source
theorem Int.odd_pow' {m : ℤ} {n : ℕ} (h : n ≠ 0) :
Odd (m ^ n) ↔ Odd m
source
theorem Int.odd_add {m n : ℤ} :
Odd (m + n) ↔ (Odd m ↔ Even n)
source
theorem Int.odd_add' {m n : ℤ} :
Odd (m + n) ↔ (Odd n ↔ Even m)
source
theorem Int.ne_of_odd_add {m n : ℤ} (h : Odd (m + n)) :
m ≠ n
source
theorem Int.odd_sub {m n : ℤ} :
Odd (m - n) ↔ (Odd m ↔ Even n)
source
theorem Int.odd_sub' {m n : ℤ} :
Odd (m - n) ↔ (Odd n ↔ Even m)
source
theorem Int.even_mul_succ_self (n : ℤ) :
Even (n * (n + 1))
source
theorem Int.even_mul_pred_self (n : ℤ) :
Even (n * (n - 1))
source
@[simp]
theorem Int.odd_coe_nat (n : ℕ) :
Odd ↑n ↔ Odd n
source
@[simp]
theorem Int.natAbs_even {n : ℤ} :
Even n.natAbs ↔ Even n
source
@[simp]
theorem Int.natAbs_odd {n : ℤ} :
Odd n.natAbs ↔ Odd n
source
theorem Even.natAbs {n : ℤ} :
Even n → Even n.natAbs

Alias of the reverse direction of Int.natAbs_even.

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

Alias of the reverse direction of Int.natAbs_odd.

source
theorem Int.four_dvd_add_or_sub_of_odd {a b : ℤ} (ha : Odd a) (hb : Odd b) :
4 ∣ a + b ∨ 4 ∣ a - b
source
theorem Int.two_dvd_mul_add_one (k : ℤ) :
2 ∣ k * (k + 1)
source
theorem Int.two_mul_ediv_two_add_one_of_odd {n : ℤ} :
Odd n → 2 * (n / 2) + 1 = n
source
theorem Int.ediv_two_mul_two_add_one_of_odd {n : ℤ} :
Odd n → n / 2 * 2 + 1 = n
source
theorem Int.add_one_ediv_two_mul_two_of_odd {n : ℤ} :
Odd n → 1 + n / 2 * 2 = n
source
theorem Int.two_mul_ediv_two_of_odd {n : ℤ} (h : Odd n) :
2 * (n / 2) = n - 1
source
@[simp]
theorem Int.even_sign_iff {z : ℤ} :
Even z.sign ↔ z = 0
source
@[simp]
theorem Int.odd_sign_iff {z : ℤ} :
Odd z.sign ↔ z ≠ 0
source
@[simp]
theorem Int.isSquare_natCast_iff {n : ℕ} :
IsSquare ↑n ↔ IsSquare n
source
@[simp]
theorem Int.isSquare_ofNat_iff {n : ℕ} :
IsSquare (OfNat.ofNat n) ↔ IsSquare (OfNat.ofNat n)
source
theorem Int.natCast_pow_pred (b p : ℕ) (w : 0 < b) :
↑(b ^ p - 1) = ↑b ^ p - 1
source
theorem Int.coe_nat_two_pow_pred (p : ℕ) :
↑(2 ^ p - 1) = 2 ^ p - 1
source
theorem Odd.neg_zpow {α : Type u_1} [DivisionMonoid α] [HasDistribNeg α] {n : ℤ} (h : Odd n) (a : α) :
(-a) ^ n = -a ^ n
source
theorem Odd.neg_one_zpow {α : Type u_1} [DivisionMonoid α] [HasDistribNeg α] {n : ℤ} (h : Odd n) :
(-1) ^ n = -1