Mathlib.Data.Int.Parity._auxLemma.26
theorem Mathlib.Data.Int.Parity._auxLemma.26 : ∀ {n : ℤ}, Even (n - 1) = ¬Even n
The theorem `Mathlib.Data.Int.Parity._auxLemma.26` states that for any two integers `m` and `n`, the product `m * n` is even if and only if either `m` or `n` (or both) are even. Here, an integer `a` is said to be 'even' if there exists another integer `r` such that `a = r + r`.
More concisely: The theorem `Mathlib.Data.Int.Parity._auxLemma.26` asserts that the product of two integers `m` and `n` is even if and only if at least one of them is even.
|
Int.even_iff
theorem Int.even_iff : ∀ {n : ℤ}, Even n ↔ n % 2 = 0
This theorem states that for any integer `n`, `n` is even if and only if `n` modulo 2 equals 0. In other words, an integer `n` satisfies the property `Even`--meaning there exists some other integer `r` such that `n = r + r`--if and only if the remainder when `n` is divided by 2 is 0. This is a formalization of the usual mathematical definition of even numbers in the integers.
More concisely: An integer `n` is even if and only if `n` modulo 2 equals 0.
|
Even.natAbs
theorem Even.natAbs : ∀ {n : ℤ}, Even n → Even n.natAbs
The theorem `Even.natAbs` states that for all integers `n`, if `n` is an even number (i.e., it can be expressed as double of some integer), then the absolute value of `n` is also even. This theorem is an alias for the reverse direction of `Int.natAbs_even`.
More concisely: If a natural number is even, then its absolute value is even.
|
Odd.natAbs
theorem Odd.natAbs : ∀ {n : ℤ}, Odd n → Odd n.natAbs
This theorem states that for any integer `n`, if `n` is odd, then the absolute value of `n` is also odd. In other words, if there exists an integer `k` such that `n = 2*k + 1`, then there also exists an integer `k'` such that the absolute value of `n = |n| = 2*k' + 1`. This is an alias of the reverse direction of the theorem `Int.natAbs_odd` in Lean 4.
More concisely: If an integer `n` is odd, then its absolute value `|n|` is also odd.
|
Int.even_or_odd
theorem Int.even_or_odd : ∀ (n : ℤ), Even n ∨ Odd n
This theorem states that for every integer `n`, `n` is either even or odd. In the context of the defined terms, an integer is even if it can be expressed as twice some integer, i.e., `n = 2*r` for some integer `r`. On the other hand, an integer is odd if it can be expressed in the form `n = 2*k + 1` for some integer `k`. This theorem is a reflection of the fundamental dichotomy of integers into even and odd numbers.
More concisely: Every integer can be classified as even (being expressible as 2*r for some integer r) or odd (being expressible as 2*k + 1 for some integer k).
|
Int.even_sub
theorem Int.even_sub : ∀ {m n : ℤ}, Even (m - n) ↔ (Even m ↔ Even n)
This theorem states that for all integers `m` and `n`, `m - n` is even if and only if `m` is even if and only if `n` is even. In mathematical terms, it asserts that an integer subtraction `m - n` is even if and only if the integers `m` and `n` are both either even or odd.
More concisely: For integers `m` and `n`, `m - n` is even if and only if both `m` and `n` are even or odd.
|
Mathlib.Data.Int.Parity._auxLemma.21
theorem Mathlib.Data.Int.Parity._auxLemma.21 : ∀ {n : ℤ}, Even n = (n % 2 = 0)
This theorem states that for any two integers `m` and `n`, the quantity `m + n` is even if and only if `m` and `n` are both even. Here, an element `a` is defined as even if there exists a number `r` such that `a = r + r`.
More concisely: The sum of two integers is even if and only if both integers are even.
|
Int.odd_iff_not_even
theorem Int.odd_iff_not_even : ∀ {n : ℤ}, Odd n ↔ ¬Even n
This theorem states that for all integers `n`, `n` is odd if and only if `n` is not even. Here, an integer `n` is considered odd if there exists an integer `k` such that `n` equals `2*k + 1` and `n` is considered even if there exists an `r` such that `n` equals `r + r`. The theorem establishes the logical equivalence between these two conditions, meaning that `n` cannot be both odd and even at the same time.
More concisely: An integer `n` is odd if and only if it is not even. Equivalently, `n` is odd if and only if it can be written in the form `2*k + 1` for some integer `k`, and it is even if and only if it can be written in the form `r + r` for some integer `r`.
|
Mathlib.Data.Int.Parity._auxLemma.4
theorem Mathlib.Data.Int.Parity._auxLemma.4 : ∀ {n : ℤ}, Odd n = ¬Even n
The theorem `Mathlib.Data.Int.Parity._auxLemma.4` states that for any integer `n`, `n` is odd if and only if `n` is not even. In mathematical terms, an integer `n` is considered odd (as per the given definition) if there exists another integer `k` such that `n = 2*k + 1`, and it is considered even if there exists an integer `r` such that `n = r + r`. The theorem establishes the mutual exclusivity of these two properties, meaning an integer can't be both odd and even at the same time.
More concisely: An integer is odd if and only if it is not even. In other words, an integer is odd if and only if it cannot be expressed as the sum of two equal integers.
|
Mathlib.Data.Int.Parity._auxLemma.19
theorem Mathlib.Data.Int.Parity._auxLemma.19 : ∀ {α : Sort u_1} {a b : α}, (a = b) = (b = a)
This theorem, `Mathlib.Data.Int.Parity._auxLemma.19`, states that the integer 1 is not even. In the context of this theorem, a number is defined as even if it can be expressed as the sum of two identical numbers. However, there is no integer that, when doubled, equals 1, hence 1 is not considered even under this definition.
More concisely: The theorem `Mathlib.Data.Int.Parity._auxLemma.19` in Lean 4 asserts that the integer 1 is odd, since it cannot be expressed as the sum of two identical integers.
|
Int.even_iff_not_odd
theorem Int.even_iff_not_odd : ∀ {n : ℤ}, Even n ↔ ¬Odd n
The theorem `Int.even_iff_not_odd` states that for every integer `n`, `n` is even if and only if `n` is not odd. Here, an integer `n` is defined as "even" if it can be expressed as the sum of two identical integers, and "odd" if it can be written in the form `2*k + 1` for some integer `k`. This theorem formalizes a basic property of integers in the mathematical field of number theory.
More concisely: An integer is even if and only if it is not odd, where an integer is even if it can be expressed as the sum of two identical integers, and odd if it can be written in the form 2*k + 1 for some integer k.
|