Sum of the finite geometric series $\sum_{i=0}^{n-1} x^i$.
Equations
- geom_series x n = (finset.range n).sum (λ (i : ℕ), x ^ i)
theorem
geom_series_def
{α : Type u}
[semiring α]
(x : α)
(n : ℕ) :
geom_series x n = (finset.range n).sum (λ (i : ℕ), x ^ i)
@[simp]
theorem
op_geom_series
{α : Type u}
[ring α]
(x : α)
(n : ℕ) :
opposite.op (geom_series x n) = geom_series (opposite.op x) n
Sum of the finite geometric series $\sum_{i=0}^{n-1} x^i y^{n-1-i}$.
Equations
- geom_series₂ x y n = (finset.range n).sum (λ (i : ℕ), x ^ i * y ^ (n - 1 - i))
theorem
geom_series₂_def
{α : Type u}
[semiring α]
(x y : α)
(n : ℕ) :
geom_series₂ x y n = (finset.range n).sum (λ (i : ℕ), x ^ i * y ^ (n - 1 - i))
@[simp]
@[simp]
@[simp]
theorem
geom_series₂_with_one
{α : Type u}
[semiring α]
(x : α)
(n : ℕ) :
geom_series₂ x 1 n = geom_series x n
$x^n-y^n = (x-y) \sum x^ky^{n-1-k}$ reformulated without - signs.
theorem
ring_hom.map_geom_series
{α : Type u}
{β : Type u_1}
[semiring α]
[semiring β]
(x : α)
(n : ℕ)
(f : α →+* β) :
⇑f (geom_series x n) = geom_series (⇑f x) n
theorem
ring_hom.map_geom_series₂
{α : Type u}
{β : Type u_1}
[semiring α]
[semiring β]
(x y : α)
(n : ℕ)
(f : α →+* β) :
⇑f (geom_series₂ x y n) = geom_series₂ (⇑f x) (⇑f y) n