Mathlib.Algebra.Group.Int.Even

Int.emod_two_ne_one theorem

: ¬n % 2 = 1 ↔ n % 2 = 0

Full source

@[simp] lemma emod_two_ne_one : ¬n % 2 = 1¬n % 2 = 1 ↔ n % 2 = 0 := by
  rcases emod_two_eq_zero_or_one n with h | h <;> simp [h]

Characterization of Even Integers via Modulo 2

Informal description

For any integer $n$, the remainder of $n$ modulo $2$ is not equal to $1$ if and only if the remainder of $n$ modulo $2$ is equal to $0$.

Int.one_emod_two theorem

: (1 : Int) % 2 = 1

Full source

@[simp] lemma one_emod_two : (1 : Int) % 2 = 1 := rfl

Modulo Identity: $1 \bmod 2 = 1$

Informal description

The integer 1 modulo 2 equals 1, i.e., $1 \bmod 2 = 1$.

Int.emod_two_ne_zero theorem

: ¬n % 2 = 0 ↔ n % 2 = 1

Full source

@[local simp] lemma emod_two_ne_zero : ¬n % 2 = 0¬n % 2 = 0 ↔ n % 2 = 1 := by
  rcases emod_two_eq_zero_or_one n with h | h <;> simp [h]

Characterization of Odd Integers via Modulo 2

Informal description

For any integer $n$, the remainder of $n$ modulo $2$ is not equal to $0$ if and only if the remainder of $n$ modulo $2$ is equal to $1$.

Int.even_iff theorem

: Even n ↔ n % 2 = 0

Full source

lemma even_iff : EvenEven n ↔ n % 2 = 0 where
  mp := fun ⟨m, hm⟩ ↦ by simp [← Int.two_mul, hm]
  mpr h := ⟨n / 2, (emod_add_ediv n 2).symm.trans (by simp [← Int.two_mul, h])⟩

Characterization of Even Integers via Modulo 2

Informal description

An integer $n$ is even if and only if $n$ modulo 2 equals 0, i.e., $n \bmod 2 = 0$.

Int.not_even_iff theorem

: ¬Even n ↔ n % 2 = 1

Full source

lemma not_even_iff : ¬Even n¬Even n ↔ n % 2 = 1 := by rw [even_iff, emod_two_ne_zero]

Characterization of Odd Integers via Non-Evenness

Informal description

An integer $n$ is not even if and only if the remainder of $n$ modulo $2$ is equal to $1$, i.e., $\neg \text{Even}(n) \leftrightarrow n \bmod 2 = 1$.

Int.two_dvd_ne_zero theorem

: ¬2 ∣ n ↔ n % 2 = 1

Full source

@[simp] lemma two_dvd_ne_zero : ¬2 ∣ n¬2 ∣ n ↔ n % 2 = 1 :=
  (even_iff_exists_two_nsmul _).symm.not.trans not_even_iff

Characterization of Non-Divisibility by 2 via Modulo 2

Informal description

An integer $n$ is not divisible by $2$ if and only if the remainder of $n$ modulo $2$ is equal to $1$, i.e., $\neg (2 \mid n) \leftrightarrow n \bmod 2 = 1$.

Int.instDecidablePredEven instance

: DecidablePred (Even : ℤ → Prop)

Full source

instance : DecidablePred (Even : ℤ → Prop) := fun _ ↦ decidable_of_iff _ even_iff.symm

Decidability of Evenness for Integers

Informal description

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

Int.instDecidablePredIsSquare instance

: DecidablePred (IsSquare : ℤ → Prop)

Full source

/-- `IsSquare` can be decided on `ℤ` by checking against the square root. -/
instance : DecidablePred (IsSquare : ℤ → Prop) :=
  fun m ↦ decidable_of_iff' (sqrt m * sqrt m = m) <| by
    simp_rw [← exists_mul_self m, IsSquare, eq_comm]

Decidability of Perfect Squares for Integers

Informal description

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

Int.not_even_one theorem

: ¬Even (1 : ℤ)

Full source

@[simp] lemma not_even_one : ¬Even (1 : ℤ) := by simp [even_iff]

One is Not Even

Informal description

The integer $1$ is not even, i.e., $\neg \text{Even}(1)$.

Int.even_add theorem

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

Full source

@[parity_simps] lemma even_add : EvenEven (m + n) ↔ (Even m ↔ Even n) := by
  rcases emod_two_eq_zero_or_one m with h₁ | h₁ <;>
  rcases emod_two_eq_zero_or_one n with h₂ | h₂ <;>
  simp [even_iff, h₁, h₂, Int.add_emod, one_add_one_eq_two, emod_self]

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

Informal description

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

Int.two_not_dvd_two_mul_add_one theorem

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

Full source

lemma two_not_dvd_two_mul_add_one (n : ℤ) : ¬2 ∣ 2 * n + 1 := by simp [add_emod]

Odd integers are not divisible by 2

Informal description

For any integer $n$, the integer $2n + 1$ is not divisible by 2.

Int.even_sub theorem

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

Full source

@[parity_simps]
lemma even_sub : EvenEven (m - n) ↔ (Even m ↔ Even n) := by simp [sub_eq_add_neg, parity_simps]

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

Informal description

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

Int.even_add_one theorem

: Even (n + 1) ↔ ¬Even n

Full source

@[parity_simps] lemma even_add_one : EvenEven (n + 1) ↔ ¬Even n := by simp [even_add]

Parity of Successor: $n + 1$ is even iff $n$ is odd

Informal description

For any integer $n$, the integer $n + 1$ is even if and only if $n$ is not even.

Int.even_sub_one theorem

: Even (n - 1) ↔ ¬Even n

Full source

@[parity_simps] lemma even_sub_one : EvenEven (n - 1) ↔ ¬Even n := by simp [even_sub]

Evenness of $n-1$ is equivalent to oddness of $n$

Informal description

For any integer $n$, the integer $n - 1$ is even if and only if $n$ is not even, i.e., $\text{Even}(n - 1) \leftrightarrow \neg \text{Even}(n)$.

Int.even_mul theorem

: Even (m * n) ↔ Even m ∨ Even n

Full source

@[parity_simps] lemma even_mul : EvenEven (m * n) ↔ Even m ∨ Even n := by
  rcases emod_two_eq_zero_or_one m with h₁ | h₁ <;>
  rcases emod_two_eq_zero_or_one n with h₂ | h₂ <;>
  simp [even_iff, h₁, h₂, Int.mul_emod]

Evenness of Integer Product: $m \cdot n$ is even iff $m$ or $n$ is even

Informal description

For any integers $m$ and $n$, the product $m \cdot n$ is even if and only if at least one of $m$ or $n$ is even.

Int.even_pow theorem

{n : ℕ} : Even (m ^ n) ↔ Even m ∧ n ≠ 0

Full source

@[parity_simps] lemma even_pow {n : ℕ} : EvenEven (m ^ n) ↔ Even m ∧ n ≠ 0 := by
  induction n <;> simp [*, even_mul, pow_succ]; tauto

Evenness of Integer Power: $m^n$ is even iff $m$ is even and $n \neq 0$

Informal description

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

Int.even_pow' theorem

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

Full source

lemma even_pow' {n : ℕ} (h : n ≠ 0) : EvenEven (m ^ n) ↔ Even m := even_pow.trans <| and_iff_left h

Evenness of Integer Power with Nonzero Exponent: $m^n$ is even iff $m$ is even for $n \neq 0$

Informal description

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

Int.even_coe_nat theorem

(n : ℕ) : Even (n : ℤ) ↔ Even n

Full source

@[simp, norm_cast] lemma even_coe_nat (n : ℕ) : EvenEven (n : ℤ) ↔ Even n := by
  rw_mod_cast [even_iff, Nat.even_iff]

Evenness Preservation Between Natural Numbers and Integers

Informal description

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

Int.two_mul_ediv_two_of_even theorem

: Even n → 2 * (n / 2) = n

Full source

lemma two_mul_ediv_two_of_even : Even n → 2 * (n / 2) = n :=
  fun h ↦ Int.mul_ediv_cancel' ((even_iff_exists_two_nsmul _).mp h)

Even Integer Property: $2 \cdot (n/2) = n$ for even $n$

Informal description

For any integer $n$, if $n$ is even, then $2 \cdot (n / 2) = n$.

Int.ediv_two_mul_two_of_even theorem

: Even n → n / 2 * 2 = n

Full source

lemma ediv_two_mul_two_of_even : Even n → n / 2 * 2 = n :=
  fun h ↦ Int.ediv_mul_cancel ((even_iff_exists_two_nsmul _).mp h)

Division-Multiplication Identity for Even Integers

Informal description

For any even integer $n$, the product of $n/2$ and $2$ equals $n$, i.e., $\frac{n}{2} \times 2 = n$.