Mathlib.Data.Nat.Parity._auxLemma.3
theorem Mathlib.Data.Nat.Parity._auxLemma.3 : ∀ {α : Type u} [inst : NonAssocSemiring α] (n : α), n + n = 2 * n := by
sorry
This theorem, `Mathlib.Data.Nat.Parity._auxLemma.3`, states that for any type `α` that has a non-associative semiring structure, the sum of any element `n` with itself is equal to twice `n`. In terms of mathematical notation, this theorem expresses the equation `n + n = 2 * n` for all `n` in the non-associative semiring.
More concisely: In any non-associative semiring, the sum of any element with itself equals twice that element.
|
Nat.odd_iff
theorem Nat.odd_iff : ∀ {n : ℕ}, Odd n ↔ n % 2 = 1
This theorem establishes an equivalence for a natural number `n` to be considered odd in two different ways. According to the theorem, a natural number `n` is odd if and only if `n` modulo 2 equals 1. This is equivalent to the definition of oddness in semirings, where an element `a` of a semiring is considered odd if there exists a `k` such that `a` is equal to `2*k + 1`.
More concisely: A natural number `n` is equivalent to being odd, as defined in Lean 4, if and only if `n` modulo 2 equals 1, which is equivalent to `n` being expressible as `2*k + 1` for some natural number `k`.
|
Odd.ne_two_of_dvd_nat
theorem Odd.ne_two_of_dvd_nat : ∀ {m n : ℕ}, Odd n → m ∣ n → m ≠ 2
The theorem `Odd.ne_two_of_dvd_nat` asserts that for all natural numbers `m` and `n`, if `n` is an odd number, and `m` divides `n`, then `m` cannot be `2`. This means that `2` cannot be a factor of an odd number. In more mathematical terms, for all natural numbers `m` and `n`, if there exists a natural number `k` such that `n = 2*k + 1` (implying `n` is odd) and `m` divides `n`, then `m` must not equal `2`.
More concisely: For all natural numbers `m` and `n`, if `n` is odd and `m` divides `n`, then `m` does not equal `2`.
|
Mathlib.Data.Nat.Parity._auxLemma.10
theorem Mathlib.Data.Nat.Parity._auxLemma.10 : ∀ {n : ℕ}, (¬2 ∣ n) = (n % 2 = 1)
This theorem states that the number 1 is not even. In the context of the definitions provided, an even number is defined as a number `a` that can be expressed as `a = r + r`, for some `r`. The theorem asserts that no such `r` exists for `a = 1`, i.e., 1 cannot be expressed as the sum of two identical numbers.
More concisely: The theorem asserts that 1 cannot be expressed as the sum of two identical numbers, making it an odd number in the given definition of even and odd numbers.
|
Odd.mod_even
theorem Odd.mod_even : ∀ {n a : ℕ}, Odd n → Even a → Odd (n % a)
This theorem states that if a natural number `n` is odd and another natural number `a` is even, then the remainder when `n` is divided by `a` (denoted as `n % a`) is also odd. Specifically, in mathematical terms, this means that if `n = 2*k + 1` for some natural number `k` (which makes `n` odd), and `a = r + r` for some natural number `r` (which makes `a` even), then there exists a natural number `m` such that `n % a = 2*m + 1`, i.e., `n % a` is odd.
More concisely: If a natural number `n` is odd and another natural number `a` is even, then the remainder `n % a` is an odd number.
|
Nat.even_pow
theorem Nat.even_pow : ∀ {m n : ℕ}, Even (m ^ n) ↔ Even m ∧ n ≠ 0
The theorem `Nat.even_pow` states that for any two natural numbers `m` and `n`, the statement "The number `m` raised to the power `n` is even" is equivalent to the statement "The number `m` is even and `n` is not zero". Here, a number is considered even if it can be expressed as the sum of two identical numbers (in other words, it is a multiple of 2).
More concisely: For all natural numbers m and n, m^n is even if and only if m is even and n is not zero.
|
Nat.even_iff
theorem Nat.even_iff : ∀ {n : ℕ}, Even n ↔ n % 2 = 0
This theorem states that for any natural number `n`, `n` is even if and only if the remainder when `n` is divided by 2 equals 0. In other words, this theorem provides a condition to check the evenness of a number in terms of a modular arithmetic operation. Specifically, a natural number `n` satisfies `Even n` (meaning there exists a natural number `r` such that `n = r + r`) if and only if `n` modulo 2 equals zero.
More concisely: A natural number `n` is even if and only if `n` modulo 2 equals 0.
|
Nat.even_sub
theorem Nat.even_sub : ∀ {m n : ℕ}, n ≤ m → (Even (m - n) ↔ (Even m ↔ Even n))
The theorem `Nat.even_sub` states that for any two natural numbers `m` and `n` with `n` less than or equal to `m`, the difference `m - n` is even if and only if both `m` and `n` are either even or odd. In mathematical terms, this can be written as: for all natural numbers m and n with n ≤ m, m - n is even if and only if m and n are both even or both odd.
More concisely: For all natural numbers m and n with n <= m, m - n is even if and only if both m and n are even or odd.
|
Even.mod_even
theorem Even.mod_even : ∀ {n a : ℕ}, Even n → Even a → Even (n % a)
The theorem `Even.mod_even` states that for any two natural numbers `n` and `a`, if both `n` and `a` are even (i.e., each can be expressed as twice some other natural number), then the remainder when `n` is divided by `a` is also even.
More concisely: If both `n` and `a` are even natural numbers, then the remainder of `n` divided by `a` is also even.
|
Nat.even_add
theorem Nat.even_add : ∀ {m n : ℕ}, Even (m + n) ↔ (Even m ↔ Even n)
This theorem states that for all natural numbers `m` and `n`, the sum `m + n` is even if and only if `m` and `n` are both even or both odd. In other words, the parity of the sum of two natural numbers is the same as the parity of the individual numbers. Here, `Even` is a property of a number that is defined to be true if the number can be expressed as the sum of two equal numbers.
More concisely: The sum of two natural numbers is even if and only if both numbers are even or both are odd.
|
Even.mod_even_iff
theorem Even.mod_even_iff : ∀ {n a : ℕ}, Even a → (Even (n % a) ↔ Even n)
The theorem `Even.mod_even_iff` states that for any two natural numbers `n` and `a`, if `a` is an even number, then `n` is also an even number if and only if the remainder of `n` divided by `a` is an even number. Here, a number is defined as even if it can be written as twice some other number.
More concisely: For any natural numbers n and a, n is even if and only if a is even implies the remainder of n divided by a is even.
|
Mathlib.Data.Nat.Parity._auxLemma.4
theorem Mathlib.Data.Nat.Parity._auxLemma.4 : ∀ {α : Sort u_1} {a b : α}, (a = b) = (b = a)
This theorem states that for all natural numbers `n`, `n` is odd if and only if it is not even. In the context of a semiring, a number `n` is odd if there exists another number `k` such that `n` equals `2*k + 1`. On the other hand, a number `n` is even if there exists a number `r` such that `n` equals `r + r`. Therefore, this theorem establishes the mutually exclusive and exhaustive nature of odd and even numbers in the set of natural numbers.
More concisely: A natural number `n` is odd if and only if it cannot be expressed as the sum of two equal natural numbers. Equivalently, it is odd if and only if it is of the form `2*k + 1` for some natural number `k`.
|
Nat.even_or_odd
theorem Nat.even_or_odd : ∀ (n : ℕ), Even n ∨ Odd n
This theorem states that for every natural number `n`, the number is either even or odd. A natural number `n` is defined as even if it can be expressed as the sum of two identical numbers, and as odd if it can be expressed as `2*k + 1` for some number `k`. Thus, the theorem asserts that any natural number fits one of these two definitions.
More concisely: Every natural number can be expressed as an even number (the sum of two identical numbers) or an odd number (2 times an integer plus 1).
|
Nat.even_iff_not_odd
theorem Nat.even_iff_not_odd : ∀ {n : ℕ}, Even n ↔ ¬Odd n
This theorem states that for every natural number `n`, `n` is even if and only if `n` is not odd. Here, a number is defined as being even if it can be expressed as the sum of two identical numbers, and as being odd if it can be represented as `2*k + 1` for some natural number `k`. In other words, a natural number cannot be both even and odd simultaneously.
More concisely: A natural number is even if and only if it is not odd. Equivalently, a natural number is even if and only if it can be written as 2 times some natural number, and it is odd if and only if it can be written as 2 times some natural number plus 1.
|
Nat.odd_iff_not_even
theorem Nat.odd_iff_not_even : ∀ {n : ℕ}, Odd n ↔ ¬Even n
This theorem states that for every natural number `n`, `n` being odd is equivalent to `n` not being even. In other words, a natural number is odd if and only if it is not even. Here, a number is considered odd if it can be expressed as `2*k + 1` for some `k`, and a number is considered even if it can be written as `r + r` for some `r`.
More concisely: A natural number is odd if and only if it is not even, or equivalently, a natural number is odd if and only if it can be expressed as 2 times an integer plus one, while an even number can be expressed as the sum of two integers.
|
Mathlib.Data.Nat.Parity._auxLemma.13
theorem Mathlib.Data.Nat.Parity._auxLemma.13 : ∀ {m n : ℕ}, Even (m + n) = (Even m ↔ Even n)
This theorem states that for any natural number `n`, the number `n + 1` is even if and only if `n` is not even. In other words, if `n` is an odd number, then `n + 1` is an even number, and vice versa.
More concisely: For any natural number `n`, `n + 1` is even if and only if `n` is odd.
|
Nat.even_mul_self_pred
theorem Nat.even_mul_self_pred : ∀ (n : ℕ), Even (n * (n - 1))
This theorem states that for all natural numbers `n`, the product of `n` and `n - 1` is an even number. In mathematical terms, this theorem can be written as: "∀ n ∈ ℕ, n*(n - 1) is even." Here, a number is considered even if it can be expressed as twice another number, in this case, n*(n - 1) = 2*r for some `r`.
More concisely: For all natural numbers `n`, the product of `n` and `n-1` is an even number. Equivalently, the product of two consecutive natural numbers is an even number.
|
Odd.mod_even_iff
theorem Odd.mod_even_iff : ∀ {n a : ℕ}, Even a → (Odd (n % a) ↔ Odd n)
The theorem `Odd.mod_even_iff` states that for any two natural numbers `n` and `a`, if `a` is even, then `n` is odd if and only if the remainder when `n` is divided by `a` is odd. In other words, in the context of natural numbers with even `a`, the oddness of `n` is equivalent to the oddness of `n modulo a`.
More concisely: For any natural numbers n and even a, n is odd if and only if the remainder of n divided by a is odd.
|