Mathlib.Algebra.Ring.Int.Parity

Int.odd_iff theorem

: Odd n ↔ n % 2 = 1

Full source

lemma odd_iff : OddOdd n ↔ n % 2 = 1 where
  mp := fun ⟨m, hm⟩ ↦ by simp [hm, add_emod]
  mpr h := ⟨n / 2, by rw [← h, add_comm, emod_add_ediv n 2]⟩

Characterization of Odd Integers via Modulo 2

Informal description

An integer $n$ is odd if and only if the remainder when $n$ is divided by $2$ is $1$, i.e., $n \equiv 1 \mod 2$.

Int.not_odd_iff theorem

: ¬Odd n ↔ n % 2 = 0

Full source

lemma not_odd_iff : ¬Odd n¬Odd n ↔ n % 2 = 0 := by rw [odd_iff, emod_two_ne_one]

Characterization of Non-Odd Integers via Modulo 2

Informal description

For any integer $n$, the statement that $n$ is not odd is equivalent to the statement that the remainder of $n$ divided by $2$ is $0$, i.e., $\neg \text{Odd}(n) \leftrightarrow n \equiv 0 \mod 2$.

Int.not_odd_zero theorem

: ¬Odd (0 : ℤ)

Full source

@[simp] lemma not_odd_zero : ¬Odd (0 : ℤ) := not_odd_iff.mpr rfl

Zero is Not Odd

Informal description

The integer $0$ is not odd.

Int.not_odd_iff_even theorem

: ¬Odd n ↔ Even n

Full source

@[simp] lemma not_odd_iff_even : ¬Odd n¬Odd n ↔ Even n := by rw [not_odd_iff, even_iff]

Equivalence of Non-Oddness and Evenness for Integers

Informal description

For any integer $n$, the statement that $n$ is not odd is equivalent to the statement that $n$ is even, i.e., $\neg \text{Odd}(n) \leftrightarrow \text{Even}(n)$.

Int.not_even_iff_odd theorem

: ¬Even n ↔ Odd n

Full source

@[simp] lemma not_even_iff_odd : ¬Even n¬Even n ↔ Odd n := by rw [not_even_iff, odd_iff]

Equivalence of Non-Evenness and Oddness for Integers

Informal description

An integer $n$ is not even if and only if it is odd.

Int.even_or_odd theorem

(n : ℤ) : Even n ∨ Odd n

Full source

lemma even_or_odd (n : ℤ) : EvenEven n ∨ Odd n := Or.imp_right not_even_iff_odd.1 <| em <| Even n

Every Integer is Even or Odd

Informal description

For any integer $n$, either $n$ is even or $n$ is odd.

Int.even_or_odd' theorem

(n : ℤ) : ∃ k, n = 2 * k ∨ n = 2 * k + 1

Full source

lemma even_or_odd' (n : ℤ) : ∃ k, n = 2 * k ∨ n = 2 * k + 1 := by
  simpa only [two_mul, exists_or, Odd, Even] using even_or_odd n

Existence of Integer Representation as Even or Odd

Informal description

For every integer $n$, there exists an integer $k$ such that either $n = 2k$ or $n = 2k + 1$.

Int.even_xor'_odd theorem

(n : ℤ) : Xor' (Even n) (Odd n)

Full source

lemma even_xor'_odd (n : ℤ) : Xor' (Even n) (Odd n) := by
  cases even_or_odd n with
  | inl h => exact Or.inl ⟨h, not_odd_iff_even.2 h⟩
  | inr h => exact Or.inr ⟨h, not_even_iff_odd.2 h⟩

Exclusive Disjunction of Even and Odd for Integers

Informal description

For any integer $n$, exactly one of the following holds: $n$ is even or $n$ is odd.

Int.even_xor'_odd' theorem

(n : ℤ) : ∃ k, Xor' (n = 2 * k) (n = 2 * k + 1)

Full source

lemma even_xor'_odd' (n : ℤ) : ∃ k, Xor' (n = 2 * k) (n = 2 * k + 1) := by
  rcases even_or_odd n with (⟨k, rfl⟩ | ⟨k, rfl⟩) <;> use k
  · simpa only [← two_mul, Xor', true_and, eq_self_iff_true, not_true, or_false,
      and_false] using (succ_ne_self (2 * k)).symm
  · simp only [Xor', add_eq_left, false_or, eq_self_iff_true, not_true, not_false_iff,
      one_ne_zero, and_self_iff]

Exclusive Parity of Integers: Every Integer is Even or Odd, but Not Both

Informal description

For any integer $n$, there exists an integer $k$ such that either $n = 2k$ or $n = 2k + 1$, but not both. In other words, every integer is either even or odd, but not both.

Int.instDecidablePredOdd instance

: DecidablePred (Odd : ℤ → Prop)

Full source

instance : DecidablePred (Odd : ℤ → Prop) := fun _ => decidable_of_iff _ not_even_iff_odd

Decidability of Oddness for Integers

Informal description

For any integer $n$, the property of being odd is decidable. That is, there exists an algorithm to determine whether $n$ is odd or not.

Int.even_add' theorem

: Even (m + n) ↔ (Odd m ↔ Odd n)

Full source

lemma even_add' : EvenEven (m + n) ↔ (Odd m ↔ Odd n) := by
  rw [even_add, ← not_odd_iff_even, ← not_odd_iff_even, not_iff_not]

Parity of Sum: $\text{Even}(m + n) \leftrightarrow (\text{Odd}(m) \leftrightarrow \text{Odd}(n))$

Informal description

For any integers $m$ and $n$, the sum $m + n$ is even if and only if $m$ is odd exactly when $n$ is odd. In other words, $\text{Even}(m + n) \leftrightarrow (\text{Odd}(m) \leftrightarrow \text{Odd}(n))$.

Int.not_even_two_mul_add_one theorem

(n : ℤ) : ¬Even (2 * n + 1)

Full source

lemma not_even_two_mul_add_one (n : ℤ) : ¬ Even (2 * n + 1) :=
  not_even_iff_odd.2 <| odd_two_mul_add_one n

Oddness of $2n + 1$ in Integers

Informal description

For any integer $n$, the number $2n + 1$ is not even.

Int.even_sub' theorem

: Even (m - n) ↔ (Odd m ↔ Odd n)

Full source

lemma even_sub' : EvenEven (m - n) ↔ (Odd m ↔ Odd n) := by
  rw [even_sub, ← not_odd_iff_even, ← not_odd_iff_even, not_iff_not]

Parity of Difference: $\text{Even}(m - n) \leftrightarrow (\text{Odd}(m) \leftrightarrow \text{Odd}(n))$

Informal description

For any integers $m$ and $n$, the difference $m - n$ is even if and only if $m$ is odd exactly when $n$ is odd. In other words, $\text{Even}(m - n) \leftrightarrow (\text{Odd}(m) \leftrightarrow \text{Odd}(n))$.

Int.odd_mul theorem

: Odd (m * n) ↔ Odd m ∧ Odd n

Full source

lemma odd_mul : OddOdd (m * n) ↔ Odd m ∧ Odd n := by simp [← not_even_iff_odd, not_or, parity_simps]

Odd Product Condition for Integers: $m \cdot n$ odd $\iff$ $m$ and $n$ odd

Informal description

For any integers $m$ and $n$, the product $m \cdot n$ is odd if and only if both $m$ and $n$ are odd.

Int.Odd.of_mul_left theorem

(h : Odd (m * n)) : Odd m

Full source

lemma Odd.of_mul_left (h : Odd (m * n)) : Odd m := (odd_mul.mp h).1

Odd Product Implies Odd Left Factor in Integers

Informal description

For any integers $m$ and $n$, if the product $m \cdot n$ is odd, then $m$ is odd.

Int.Odd.of_mul_right theorem

(h : Odd (m * n)) : Odd n

Full source

lemma Odd.of_mul_right (h : Odd (m * n)) : Odd n := (odd_mul.mp h).2

Oddness of Right Factor in Integer Multiplication

Informal description

For any integers $m$ and $n$, if the product $m \cdot n$ is odd, then $n$ is odd.

Int.odd_pow theorem

{n : ℕ} : Odd (m ^ n) ↔ Odd m ∨ n = 0

Full source

@[parity_simps] lemma odd_pow {n : ℕ} : OddOdd (m ^ n) ↔ Odd m ∨ n = 0 := by
  rw [← not_iff_not, not_odd_iff_even, not_or, not_odd_iff_even, even_pow]

Oddness of Integer Power: $m^n$ is odd iff $m$ is odd or $n=0$

Informal description

For any integer $m$ and natural number $n$, the power $m^n$ is odd if and only if either $m$ is odd or $n = 0$.

Int.odd_pow' theorem

{n : ℕ} (h : n ≠ 0) : Odd (m ^ n) ↔ Odd m

Full source

lemma odd_pow' {n : ℕ} (h : n ≠ 0) : OddOdd (m ^ n) ↔ Odd m := odd_pow.trans <| or_iff_left h

Oddness of Integer Power for Nonzero Exponent: $m^n$ is odd iff $m$ is odd

Informal description

For any integer $m$ and nonzero natural number $n$, the power $m^n$ is odd if and only if $m$ is odd.

Int.odd_add theorem

: Odd (m + n) ↔ (Odd m ↔ Even n)

Full source

@[parity_simps] lemma odd_add : OddOdd (m + n) ↔ (Odd m ↔ Even n) := by
  rw [← not_even_iff_odd, even_add, not_iff, ← not_even_iff_odd]

Parity of Sum: $\text{Odd}(m + n) \leftrightarrow (\text{Odd}(m) \leftrightarrow \text{Even}(n))$

Informal description

For any integers $m$ and $n$, the sum $m + n$ is odd if and only if $m$ is odd exactly when $n$ is even. In other words, $\text{Odd}(m + n) \leftrightarrow (\text{Odd}(m) \leftrightarrow \text{Even}(n))$.

Int.odd_add' theorem

: Odd (m + n) ↔ (Odd n ↔ Even m)

Full source

lemma odd_add' : OddOdd (m + n) ↔ (Odd n ↔ Even m) := by rw [add_comm, odd_add]

Parity of Sum: $\text{Odd}(m + n) \leftrightarrow (\text{Odd}(n) \leftrightarrow \text{Even}(m))$

Informal description

For any integers $m$ and $n$, the sum $m + n$ is odd if and only if $n$ is odd exactly when $m$ is even. In other words, $\text{Odd}(m + n) \leftrightarrow (\text{Odd}(n) \leftrightarrow \text{Even}(m))$.

Int.ne_of_odd_add theorem

(h : Odd (m + n)) : m ≠ n

Full source

lemma ne_of_odd_add (h : Odd (m + n)) : m ≠ n := by rintro rfl; simp [← not_even_iff_odd] at h

Distinctness of Integers with Odd Sum

Informal description

For any integers $m$ and $n$, if the sum $m + n$ is odd, then $m$ is not equal to $n$.

Int.odd_sub theorem

: Odd (m - n) ↔ (Odd m ↔ Even n)

Full source

@[parity_simps] lemma odd_sub : OddOdd (m - n) ↔ (Odd m ↔ Even n) := by
  rw [← not_even_iff_odd, even_sub, not_iff, ← not_even_iff_odd]

Odd Difference Equivalence: $\text{Odd}(m - n) \leftrightarrow (\text{Odd}(m) \leftrightarrow \text{Even}(n))$

Informal description

For any integers $m$ and $n$, the difference $m - n$ is odd if and only if $m$ is odd exactly when $n$ is even. In other words, $\text{Odd}(m - n) \leftrightarrow (\text{Odd}(m) \leftrightarrow \text{Even}(n))$.

Int.odd_sub' theorem

: Odd (m - n) ↔ (Odd n ↔ Even m)

Full source

lemma odd_sub' : OddOdd (m - n) ↔ (Odd n ↔ Even m) := by
  rw [← not_even_iff_odd, even_sub, not_iff, not_iff_comm, ← not_even_iff_odd]

Odd Difference Characterization: $\text{Odd}(m - n) \leftrightarrow (\text{Odd}(n) \leftrightarrow \text{Even}(m))$

Informal description

For any integers $m$ and $n$, the difference $m - n$ is odd if and only if $n$ is odd exactly when $m$ is even. In other words, $\text{Odd}(m - n) \leftrightarrow (\text{Odd}(n) \leftrightarrow \text{Even}(m))$.

Int.even_mul_succ_self theorem

(n : ℤ) : Even (n * (n + 1))

Full source

lemma even_mul_succ_self (n : ℤ) : Even (n * (n + 1)) := by
  simpa [even_mul, parity_simps] using n.even_or_odd

Product of Consecutive Integers is Even

Informal description

For any integer $n$, the product $n(n + 1)$ is even.

Int.even_mul_pred_self theorem

(n : ℤ) : Even (n * (n - 1))

Full source

lemma even_mul_pred_self (n : ℤ) : Even (n * (n - 1)) := by
  simpa [even_mul, parity_simps] using n.even_or_odd

Evenness of Product of Integer and Its Predecessor: $n(n-1)$ is even

Informal description

For any integer $n$, the product $n(n - 1)$ is even.

Int.odd_coe_nat theorem

(n : ℕ) : Odd (n : ℤ) ↔ Odd n

Full source

@[simp, norm_cast] lemma odd_coe_nat (n : ℕ) : OddOdd (n : ℤ) ↔ Odd n := by
  rw [← not_even_iff_odd, ← Nat.not_even_iff_odd, even_coe_nat]

Oddness Preservation Between Natural Numbers and Integers

Informal description

For any natural number $n$, the integer $n$ (viewed as an element of $\mathbb{Z}$) is odd if and only if $n$ is odd as a natural number.

Int.natAbs_even theorem

: Even n.natAbs ↔ Even n

Full source

@[simp] lemma natAbs_even : EvenEven n.natAbs ↔ Even n := by
  simp [even_iff_two_dvd, dvd_natAbs, natCast_dvd.symm]

Evenness Preservation via Absolute Value in Integers

Informal description

For any integer $n$, the absolute value of $n$ as a natural number is even if and only if $n$ itself is even. That is, $\text{Even}(|n|) \leftrightarrow \text{Even}(n)$.

Int.natAbs_odd theorem

: Odd n.natAbs ↔ Odd n

Full source

@[simp]
lemma natAbs_odd : OddOdd n.natAbs ↔ Odd n := by
  rw [← not_even_iff_odd, ← Nat.not_even_iff_odd, natAbs_even]

Oddness Preservation via Absolute Value in Integers

Informal description

For any integer $n$, the absolute value of $n$ as a natural number is odd if and only if $n$ itself is odd. That is, $\text{Odd}(|n|) \leftrightarrow \text{Odd}(n)$.

Int.four_dvd_add_or_sub_of_odd theorem

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

Full source

lemma four_dvd_add_or_sub_of_odd {a b : ℤ} (ha : Odd a) (hb : Odd b) :
    4 ∣ a + b4 ∣ a + b ∨ 4 ∣ a - b := by
  obtain ⟨m, rfl⟩ := ha
  obtain ⟨n, rfl⟩ := hb
  omega

Divisibility by 4 of Sum or Difference of Odd Integers

Informal description

For any odd integers $a$ and $b$, either $4$ divides $a + b$ or $4$ divides $a - b$.

Int.two_mul_ediv_two_add_one_of_odd theorem

: Odd n → 2 * (n / 2) + 1 = n

Full source

lemma two_mul_ediv_two_add_one_of_odd : Odd n → 2 * (n / 2) + 1 = n := by
  rintro ⟨c, rfl⟩
  rw [mul_comm]
  convert Int.ediv_add_emod' (2 * c + 1) 2
  simp [Int.add_emod]

Odd Integer Decomposition: $2 \cdot \lfloor n/2 \rfloor + 1 = n$

Informal description

For any odd integer $n$, we have $2 \cdot \lfloor n/2 \rfloor + 1 = n$.

Int.ediv_two_mul_two_add_one_of_odd theorem

: Odd n → n / 2 * 2 + 1 = n

Full source

lemma ediv_two_mul_two_add_one_of_odd : Odd n → n / 2 * 2 + 1 = n := by
  rintro ⟨c, rfl⟩
  convert Int.ediv_add_emod' (2 * c + 1) 2
  simp [Int.add_emod]

Odd Integer Decomposition: $\left\lfloor \frac{n}{2} \right\rfloor \times 2 + 1 = n$

Informal description

For any odd integer $n$, we have the identity $\left\lfloor \frac{n}{2} \right\rfloor \times 2 + 1 = n$.

Int.add_one_ediv_two_mul_two_of_odd theorem

: Odd n → 1 + n / 2 * 2 = n

Full source

lemma add_one_ediv_two_mul_two_of_odd : Odd n → 1 + n / 2 * 2 = n := by
  rintro ⟨c, rfl⟩
  rw [add_comm]
  convert Int.ediv_add_emod' (2 * c + 1) 2
  simp [Int.add_emod]

Odd Integer Decomposition: $1 + 2 \cdot \lfloor n/2 \rfloor = n$

Informal description

For any odd integer $n$, we have the identity $1 + 2 \cdot \lfloor n/2 \rfloor = n$.

Int.two_mul_ediv_two_of_odd theorem

(h : Odd n) : 2 * (n / 2) = n - 1

Full source

lemma two_mul_ediv_two_of_odd (h : Odd n) : 2 * (n / 2) = n - 1 :=
  eq_sub_of_add_eq (two_mul_ediv_two_add_one_of_odd h)

Odd Integer Property: $2 \cdot \lfloor n/2 \rfloor = n - 1$

Informal description

For any odd integer $n$, twice the floor of $n$ divided by 2 equals $n$ minus one, i.e., $2 \cdot \lfloor n/2 \rfloor = n - 1$.

Int.isSquare_natCast_iff theorem

{n : ℕ} : IsSquare (n : ℤ) ↔ IsSquare n

Full source

@[norm_cast, simp]
theorem isSquare_natCast_iff {n : ℕ} : IsSquareIsSquare (n : ℤ) ↔ IsSquare n := by
  constructor <;> rintro ⟨x, h⟩
  · exact ⟨x.natAbs, (natAbs_mul_natAbs_eq h.symm).symm⟩
  · exact ⟨x, mod_cast h⟩

Square Preservation between Natural Numbers and Integers

Informal description

For any natural number $n$, the integer $n$ (viewed as an element of $\mathbb{Z}$) is a square if and only if $n$ is a square in $\mathbb{N}$. In other words, there exists an integer $k$ such that $n = k^2$ if and only if there exists a natural number $m$ such that $n = m^2$.

Int.isSquare_ofNat_iff theorem

{n : ℕ} : IsSquare (ofNat(n) : ℤ) ↔ IsSquare (ofNat(n) : ℕ)

Full source

@[simp]
theorem isSquare_ofNat_iff {n : ℕ} :
    IsSquareIsSquare (ofNat(n) : ℤ) ↔ IsSquare (ofNat(n) : ℕ) :=
  isSquare_natCast_iff

Square Preservation under Casting from Natural Numbers to Integers

Informal description

For any natural number $n$, the integer obtained by casting $n$ (denoted as $\mathtt{ofNat}(n) : \mathbb{Z}$) is a square if and only if the natural number obtained by casting $n$ (denoted as $\mathtt{ofNat}(n) : \mathbb{N}$) is a square. In other words, there exists an integer $k$ such that $\mathtt{ofNat}(n) = k^2$ if and only if there exists a natural number $m$ such that $\mathtt{ofNat}(n) = m^2$.