# Partial sums of geometric series in a field #

This file determines the values of the geometric series $\sum_{i=0}^{n-1} x^i$ and $\sum_{i=0}^{n-1} x^i y^{n-1-i}$ and variants thereof.

## Main statements #

- `geom_sum_Ico` proves that $\sum_{i=m}^{n-1} x^i=\frac{x^n-x^m}{x-1}$ in a division ring.
- `geom_sum₂_Ico` proves that $\sum_{i=m}^{n-1} x^iy^{n - 1 - i}=\frac{x^n-y^{n-m}x^m}{x-y}$ in a field.

Several variants are recorded, generalising in particular to the case of a division ring in which `x` and `y` commute.

source
theorem Commute.geom_sum₂ {K : Type u_2} [DivisionRing K] {x y : K} (h' : Commute x y) (h : x ≠ y) (n : ℕ) :
∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
source
theorem geom_sum_eq {K : Type u_2} [DivisionRing K] {x : K} (h : x ≠ 1) (n : ℕ) :
∑ i ∈ Finset.range n, x ^ i = (x ^ n - 1) / (x - 1)
source
theorem Commute.geom_sum₂_Ico {K : Type u_2} [DivisionRing K] {x y : K} (h : Commute x y) (hxy : x ≠ y) {m n : ℕ} (hmn : m ≤ n) :
∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
source
theorem geom_sum_Ico {K : Type u_2} [DivisionRing K] {x : K} (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) :
∑ i ∈ Finset.Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)
source
theorem geom_sum_Ico' {K : Type u_2} [DivisionRing K] {x : K} (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) :
∑ i ∈ Finset.Ico m n, x ^ i = (x ^ m - x ^ n) / (1 - x)
source
theorem geom_sum_inv {K : Type u_2} [DivisionRing K] {x : K} (hx1 : x ≠ 1) (hx0 : x ≠ 0) (n : ℕ) :
∑ i ∈ Finset.range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
source
theorem geom₂_sum {K : Type u_2} [Field K] {x y : K} (h : x ≠ y) (n : ℕ) :
∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
source
theorem geom_sum₂_Ico {K : Type u_2} [Field K] {x y : K} (hxy : x ≠ y) {m n : ℕ} (hmn : m ≤ n) :
∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)