Parity of integers

Parity

@[simp]

theorem Int.emod_two_ne_one {n : ℤ} : ¬n % 2 = 1 ↔ n % 2 = 0

@[simp]

theorem Int.one_emod_two : 1 % 2 = 1

theorem Int.emod_two_ne_zero {n : ℤ} : ¬n % 2 = 0 ↔ n % 2 = 1

theorem Int.even_iff {n : ℤ} : Even n ↔ n % 2 = 0

theorem Int.not_even_iff {n : ℤ} : ¬Even n ↔ n % 2 = 1

@[simp]

theorem Int.two_dvd_ne_zero {n : ℤ} : ¬2 ∣ n ↔ n % 2 = 1

@[instance_reducible]

instance Int.instDecidablePredEven : DecidablePred Even

Equations

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

@[instance_reducible]

instance Int.instDecidablePredIsSquare : DecidablePred IsSquare

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

Equations

• m.instDecidablePredIsSquare = decidable_of_iff' (Int.sqrt m * Int.sqrt m = m) ⋯

@[simp]

theorem Int.not_even_one : ¬Even 1

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

theorem Int.two_not_dvd_two_mul_add_one (n : ℤ) : ¬2 ∣ 2 * n + 1

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

theorem Int.even_add_one {n : ℤ} : Even (n + 1) ↔ ¬Even n

theorem Int.even_sub_one {n : ℤ} : Even (n - 1) ↔ ¬Even n

theorem Int.even_mul {m n : ℤ} : Even (m * n) ↔ Even m ∨ Even n

theorem Int.even_pow {m : ℤ} {n : ℕ} : Even (m ^ n) ↔ Even m ∧ n ≠ 0

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

@[simp]

theorem Int.even_natCast (n : ℕ) : Even ↑n ↔ Even n

@[deprecated Int.even_natCast (since := "2026-10-13")]

theorem Int.even_coe_nat (n : ℕ) : Even ↑n ↔ Even n

Alias of Int.even_natCast.

theorem Int.two_mul_ediv_two_of_even {n : ℤ} : Even n → 2 * (n / 2) = n

theorem Int.ediv_two_mul_two_of_even {n : ℤ} : Even n → n / 2 * 2 = n

@[simp]

theorem Int.isSquare_sign_iff {z : ℤ} : IsSquare z.sign ↔ 0 ≤ z