Documentation

Mathlib.Algebra.Field.GeomSum

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 #

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

theorem Commute.geom_sum₂ {K : Type u_2} [DivisionRing K] {x y : K} (h' : Commute x y) (h : x y) (n : ) :
iFinset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
theorem geom_sum_eq {K : Type u_2} [DivisionRing K] {x : K} (h : x 1) (n : ) :
iFinset.range n, x ^ i = (x ^ n - 1) / (x - 1)
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) :
iFinset.Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
theorem geom_sum_Ico {K : Type u_2} [DivisionRing K] {x : K} (hx : x 1) {m n : } (hmn : m n) :
iFinset.Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)
theorem geom_sum_Ico' {K : Type u_2} [DivisionRing K] {x : K} (hx : x 1) {m n : } (hmn : m n) :
iFinset.Ico m n, x ^ i = (x ^ m - x ^ n) / (1 - x)
theorem geom_sum_inv {K : Type u_2} [DivisionRing K] {x : K} (hx1 : x 1) (hx0 : x 0) (n : ) :
iFinset.range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
theorem geom₂_sum {K : Type u_2} [Field K] {x y : K} (h : x y) (n : ) :
iFinset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
theorem geom_sum₂_Ico {K : Type u_2} [Field K] {x y : K} (hxy : x y) {m n : } (hmn : m n) :
iFinset.Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)