Commute.sub_dvd_pow_sub_pow
theorem Commute.sub_dvd_pow_sub_pow :
∀ {α : Type u} [inst : Ring α] {x y : α}, Commute x y → ∀ (n : ℕ), x - y ∣ x ^ n - y ^ n
The theorem `Commute.sub_dvd_pow_sub_pow` states that for any type `α` that forms a ring, given two elements `x` and `y` of this type that commute (meaning `x * y = y * x`), and given any natural number `n`, the difference `x - y` evenly divides the difference `x^n - y^n`. In other words, there exists some element in the ring such that multiplying it by `x - y` yields `x^n - y^n`.
More concisely: For any commuting elements $x, y$ in a ring and natural number $n$, $x^n - y^n$ is divisible by $x - y$.
|
geom_sum_succ'
theorem geom_sum_succ' :
∀ {α : Type u} [inst : Semiring α] {x : α} {n : ℕ},
((Finset.range (n + 1)).sum fun i => x ^ i) = x ^ n + (Finset.range n).sum fun i => x ^ i
The theorem `geom_sum_succ'` states that for any semiring `α`, any element `x` of `α`, and any natural number `n`, the sum of `x` to the power of each natural number in the range from 0 to `n + 1` (exclusive) is equal to `x` to the power of `n` plus the sum of `x` to the power of each natural number in the range from 0 to `n` (exclusive). In mathematical notation, this would be:
∑_{i=0}^{n+1} x^i = x^n + ∑_{i=0}^{n} x^i.
This theorem is essentially a restatement of a property of geometric progressions.
More concisely: The sum of the geometric series with first term `x` and common ratio `x` from `0` to `n+1` equals the sum of the geometric series with first term `x` and common ratio `x` from `0` to `n`, plus `x^(n+1)`.
|
Nat.geomSum_lt
theorem Nat.geomSum_lt : ∀ {m n : ℕ} {s : Finset ℕ}, 2 ≤ m → (∀ k ∈ s, k < n) → (s.sum fun k => m ^ k) < m ^ n := by
sorry
This theorem states that if you have a finite set (`Finset`) of natural numbers (`ℕ`), and all elements in this set are less than a certain number `n`, then the sum of each element raised to the power of `m` (where `m` is a natural number greater than or equal to 2) is less than `m` raised to the power of `n`.
More concisely: For any finite set `S` of natural numbers `n_i` with `n > max S.map nat.size` and any natural number `m ≥ 2`, it holds that `∑ i in S` `(n_i : ℕ) ^ m < (n : ℕ) ^ m`.
|
geom_sum_mul
theorem geom_sum_mul :
∀ {α : Type u} [inst : Ring α] (x : α) (n : ℕ), ((Finset.range n).sum fun i => x ^ i) * (x - 1) = x ^ n - 1 := by
sorry
The theorem `geom_sum_mul` states that for any ring `α` and element `x` of `α` and any natural number `n`, the sum of the `nth` powers of `x`, as `n` ranges over the natural numbers less than `n`, multiplied by `(x - 1)`, is equal to `x` raised to the power `n` minus `1`. In mathematical terms, it's expressing the formula for the sum of a geometric series: \(\sum_{i=0}^{n-1} x^i \cdot (x - 1) = x^n - 1\).
More concisely: For any ring `α` and element `x` in `α`, the sum of the `n-1` powers of `x` multiplied by `(x-1)` is equal to `x^n - 1`, where `n` is a natural number.
|
Commute.geom_sum₂_mul_add
theorem Commute.geom_sum₂_mul_add :
∀ {α : Type u} [inst : Semiring α] {x y : α},
Commute x y →
∀ (n : ℕ), ((Finset.range n).sum fun i => (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
This is a theorem about the algebraic identity $x^n-y^n = (x-y) \sum x^ky^{n-1-k}$, specifically reformulated without the use of subtraction ("-") signs. It states that for any semiring `α`, given two elements `x` and `y` of `α` that commute (meaning that `x * y = y * x`), and for every natural number `n`, the sum (`Finset.sum`) of terms `(x + y) ^ i * y ^ (n - 1 - i)` for all `i` in the range less than `n` (i.e., `0, 1, 2, ..., n-1`), multiplied by `x`, and then added to `y^n`, equals `(x + y) ^ n`. This equation holds true under the condition that `x` and `y` commute in the semiring `α`.
More concisely: For any commutative semiring `α` and elements `x, y` in `α`, the identity $(x+y)^n=\sum\_{i
|
geom_sum_succ
theorem geom_sum_succ :
∀ {α : Type u} [inst : Semiring α] {x : α} {n : ℕ},
((Finset.range (n + 1)).sum fun i => x ^ i) = (x * (Finset.range n).sum fun i => x ^ i) + 1
This theorem is called `geom_sum_succ` and it states that for any semiring `α`, any element `x` of `α`, and any natural number `n`, the sum of `x` to the power `i` for all `i` in the range from `0` to `n + 1` (inclusive of `0` but exclusive of `n + 1`) is equal to `x` times the sum of `x` to the power `i` for all `i` in the range from `0` to `n` (inclusive of `0` but exclusive of `n`), plus `1`. In mathematical notation, this theorem states that $\sum_{i=0}^{n} x^i = x \sum_{i=0}^{n-1} x^i + 1$ for all `x` in a semiring and all natural numbers `n`.
More concisely: For any semiring `α` and natural number `n`, the sum of the elements `x` raised to the power `i` for `i` from `0` to `n` is equal to `x` times the sum of `x` raised to the power `i` for `i` from `0` to `n-1`, plus `1`. In mathematical notation: $\sum\_{i=0}^n x^i = x \sum\_{i=0}^{n-1} x^i + 1$ for all `x` in a semiring.
|
Mathlib.Algebra.GeomSum._auxLemma.5
theorem Mathlib.Algebra.GeomSum._auxLemma.5 : ∀ {n : ℕ}, Even (n + 1) = ¬Even n
The theorem `Mathlib.Algebra.GeomSum._auxLemma.5` states that for any natural number `n`, the property of `n + 1` being even is equivalent to `n` being not even. In terms of mathematics, this says that if a natural number is even, then adding 1 to it makes it not even, and vice versa.
More concisely: For any natural number `n`, the parity of `n+1` is opposite to that of `n`.
|
geom_sum_eq
theorem geom_sum_eq :
∀ {α : Type u} [inst : DivisionRing α] {x : α},
x ≠ 1 → ∀ (n : ℕ), ((Finset.range n).sum fun i => x ^ i) = (x ^ n - 1) / (x - 1)
The theorem `geom_sum_eq` states that for any type `α` which forms a Division Ring and any element `x` of this type `α` that is not equal to `1`, for any natural number `n`, the sum of the `i`-th power of `x` for all `i` in the range less than `n` (also known as the geometric sum) equals `(x ^ n - 1) / (x - 1)`. In mathematical terms, for `x ≠ 1` and `n ∈ ℕ`, it asserts the equality `∑_{i=0}^{n-1} x^i = (x^n - 1) / (x - 1)`.
More concisely: For any division ring `α` and `x ∈ α \neq 1`, the geometric sum of the first `n` powers of `x`, `∑_{i=0}^{n-1} x^i`, equals `(x^n - 1) / (x - 1)` for any natural number `n`.
|
Commute.geom_sum₂_mul
theorem Commute.geom_sum₂_mul :
∀ {α : Type u} [inst : Ring α] {x y : α},
Commute x y → ∀ (n : ℕ), ((Finset.range n).sum fun i => x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
The theorem `Commute.geom_sum₂_mul` states that for any type `α` that forms a ring, given two elements `x` and `y` of this ring that commute (i.e., `x * y = y * x`), and a natural number `n`, the sum of the product of `x` raised to the `i`th power and `y` raised to the power `n - 1 - i` (where `i` ranges over natural numbers less than `n`), multiplied by the difference between `x` and `y`, is equal to `x` raised to the `n`th power minus `y` raised to the `n`th power. In mathematical notation, this is saying that:
∀ (x, y : α), (x * y = y * x) → ∀ (n : ℕ), (∑_{i=0}^{n-1} x^i * y^{n - 1 - i}) * (x - y) = x^n - y^n.
Here α is a ring, x and y are elements in α that commute, and n is a natural number.
More concisely: For any commuting elements $x, y$ in a ring $\alpha$ and natural number $n$, the sum of the geometric series $\sum\_{i=0}^{n-1} x^i y^{n-1-i}$ multiplied by the difference $x-y$ equals $x^n-y^n$.
|
Nat.geomSum_eq
theorem Nat.geomSum_eq : ∀ {m : ℕ}, 2 ≤ m → ∀ (n : ℕ), ((Finset.range n).sum fun k => m ^ k) = (m ^ n - 1) / (m - 1)
This theorem states that for any natural number `m` that is greater than or equal to 2, and for any natural number `n`, the sum of the `m` to the power of each element in the set of natural numbers less than `n` (i.e., the geometric sum) is equal to `(m ^ n - 1) / (m - 1)`. This is a specific case of the formula for the sum of a geometric series.
More concisely: For any natural number `m >= 2` and `n`, the sum of `m` raised to the power of each natural number less than `n` equals `(m ^ n - 1) / (m - 1)`.
|
geom_sum₂_mul_add
theorem geom_sum₂_mul_add :
∀ {α : Type u} [inst : CommSemiring α] (x y : α) (n : ℕ),
((Finset.range n).sum fun i => (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
The theorem `geom_sum₂_mul_add` states that for any commutative semiring `α`, and any `x`, `y` in `α`, and any natural number `n`, the equation `(∑_{i=0}^{n-1} ((x + y) ^ i * y ^ (n - 1 - i))) * x + y ^ n = (x + y) ^ n` holds true. This equation is a reformulation of the identity `x^n - y^n = (x - y) ∑_{k=0}^{n-1} x^k y^{n-1-k}` without any negative signs.
More concisely: For any commutative semiring `α` and natural number `n`, the sum `(∑_{i=0}^{n-1} (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n` equals `(x + y) ^ n`, where `x` and `y` are elements of `α`.
|
geom_sum_mul_neg
theorem geom_sum_mul_neg :
∀ {α : Type u} [inst : Ring α] (x : α) (n : ℕ), ((Finset.range n).sum fun i => x ^ i) * (1 - x) = 1 - x ^ n := by
sorry
This theorem, `geom_sum_mul_neg`, states that for every type `α` that forms a ring and any element `x` of `α` and natural number `n`, the sum of the `i-th` powers of `x` for `i` in the range of natural numbers less than `n`, multiplied by `(1 - x)`, equals `1 - x^n`. In mathematical terms, it is expressing the formula for the sum of a geometric series: $\sum_{i=0}^{n-1} x^i * (1 - x) = 1 - x^n$. This is valid in any ring structure.
More concisely: For any ring `α` and element `x` in `α`, the sum of the geometric series $\sum\_{i=0}^{n-1} x^i$ equals `1 - x^n`.
|
geom_sum_two
theorem geom_sum_two : ∀ {α : Type u} [inst : Semiring α] {x : α}, ((Finset.range 2).sum fun i => x ^ i) = x + 1 := by
sorry
The theorem `geom_sum_two` states that for any type `α` that has semiring structure and for any element `x` of `α`, the sum of `x` raised to each element in the set of natural numbers less than 2, which are 0 and 1, is equal to `x + 1`. In mathematical terms, it's stating that $x^{0} + x^{1} = x + 1$ for all `x` in a semiring.
More concisely: For any semiring `α` and its element `x`, $x^0 + x^1 = x + 1$.
|
geom_sum_pos'
theorem geom_sum_pos' :
∀ {α : Type u} {n : ℕ} {x : α} [inst : LinearOrderedRing α],
0 < x + 1 → n ≠ 0 → 0 < (Finset.range n).sum fun i => x ^ i
This theorem states that for any number `n` of type natural number and any number `x` of a type `α` that forms a linearly ordered ring, if `x + 1` is greater than 0 and `n` is not equal to 0, then the sum of `x` raised to the power of each natural number less than `n` is greater than 0. In other words, if we have a non-zero natural number `n` and a number `x` such that `x + 1` is positive, then the geometric sum `x^0 + x^1 + x^2 + ... + x^(n-1)` is also positive.
More concisely: For any non-zero natural number `n` and any element `x` in a linearly ordered ring with `x + 1 > 0`, the sum `∑ i in (0 : nat) (x ^ i)` is positive.
|
neg_one_geom_sum
theorem neg_one_geom_sum :
∀ {α : Type u} [inst : Ring α] {n : ℕ}, ((Finset.range n).sum fun i => (-1) ^ i) = if Even n then 0 else 1 := by
sorry
The theorem `neg_one_geom_sum` states that for any natural number `n` and any type `α` that forms a ring, the sum of `(-1)` raised to the power `i` as `i` ranges over all natural numbers less than `n` (essentially forming a geometric sequence with common ratio -1), is equal to 0 if `n` is even and 1 if `n` is odd. In mathematical terms, this can be written as follows: for every natural number `n`, the sum $\sum_{i=0}^{n-1} (-1)^i$ equals 0 when `n` is even and 1 when `n` is odd.
More concisely: For any natural number `n` and commutative ring `α`, the sum of `(-1)` raised to the power `i` over `i` from `0` to `n-1` equals `1` if `n` is odd and `0` if `n` is even.
|
geom_sum₂_mul
theorem geom_sum₂_mul :
∀ {α : Type u} [inst : CommRing α] (x y : α) (n : ℕ),
((Finset.range n).sum fun i => x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
This theorem, `geom_sum₂_mul`, states that for any type `α` equipped with a commutative ring structure, and for any elements `x` and `y` of this type, and a natural number `n`, the sum, over all natural numbers less than `n`, of the product of `x` raised to a given number and `y` raised to the difference between `n - 1` and that number, all multiplied by the difference `x - y`, equals the difference between `x` raised to the `n`th power and `y` raised to the `n`th power. In mathematical notation, this is:
\[
\left(\sum_{i=0}^{n-1} x^i \cdot y^{n-1-i}\right) \cdot (x - y) = x^n - y^n
\]
This is a specific form of the geometric sum formula.
More concisely: For any commutative ring `α` and natural number `n`, the geometric sum of `x^i * y^(n-1-i)` for `i` from `0` to `n-1` equals `(x^n - y^n) / (x - y)`.
|
Mathlib.Algebra.GeomSum._auxLemma.7
theorem Mathlib.Algebra.GeomSum._auxLemma.7 :
∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, (a - b = c) = (a = c + b)
This theorem, named `Mathlib.Algebra.GeomSum._auxLemma.7`, states that for any type `G` which has an `AddGroup` instance and for any three elements `a`, `b`, and `c` of type `G`: the statement "`a` minus `b` equals `c`" is equivalent to the statement "`a` equals `c` plus `b`". In mathematical terms, it confirms the principle that subtracting `b` from `a` and adding `b` to `c` are inverse operations.
More concisely: For any additive group `G` and elements `a, b, c` in `G`, `a - b = c` if and only if `a = c + b`.
|