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.
theorem
geom_sum_Ico'
{K : Type u_2}
[DivisionRing K]
{x : K}
(hx : x ≠ 1)
{m n : ℕ}
(hmn : m ≤ n)
: