mathlib docs: algebra.geom

source

def geom_series {α : Type u} [semiring α] :

α → ℕ → α

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)

source

theorem geom_series_def {α : Type u} [semiring α] (x : α) (n : ℕ) :

geom_series x n = (finset.range n).sum (λ (i : ℕ), x ^ i)

source

@[simp]

theorem geom_series_zero {α : Type u} [semiring α] (x : α) :

geom_series x 0 = 0

source

@[simp]

theorem geom_series_one {α : Type u} [semiring α] (x : α) :

geom_series x 1 = 1

source

@[simp]

theorem op_geom_series {α : Type u} [ring α] (x : α) (n : ℕ) :

opposite.op (geom_series x n) = geom_series (opposite.op x) n

source

def geom_series₂ {α : Type u} [semiring α] :

α → α → ℕ → α

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))

source

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))

source

@[simp]

theorem geom_series₂_zero {α : Type u} [semiring α] (x y : α) :

geom_series₂ x y 0 = 0

source

@[simp]

theorem geom_series₂_one {α : Type u} [semiring α] (x y : α) :

geom_series₂ x y 1 = 1

source

@[simp]

theorem geom_series₂_with_one {α : Type u} [semiring α] (x : α) (n : ℕ) :

geom_series₂ x 1 n = geom_series x n

source

theorem commute.geom_sum₂_mul_add {α : Type u} [semiring α] {x y : α} (h : commute x y) (n : ℕ) :

geom_series₂ (x + y) y n * x + y ^ n = (x + y) ^ n

$x^{n} - y^{n} = (x - y) \sum x^{k} y^{n - 1 - k}$ reformulated without - signs.

source

theorem geom_series₂_self {α : Type u_1} [comm_ring α] (x : α) (n : ℕ) :

geom_series₂ x x n = ↑n * x ^ (n - 1)

source

theorem geom_sum₂_mul_add {α : Type u} [comm_semiring α] (x y : α) (n : ℕ) :

geom_series₂ (x + y) y n * x + y ^ n = (x + y) ^ n

$x^{n} - y^{n} = (x - y) \sum x^{k} y^{n - 1 - k}$ reformulated without - signs.

source

theorem geom_sum_mul_add {α : Type u} [semiring α] (x : α) (n : ℕ) :

geom_series (x + 1) n * x + 1 = (x + 1) ^ n

source

theorem geom_sum₂_mul_comm {α : Type u} [ring α] {x y : α} (h : commute x y) (n : ℕ) :

geom_series₂ x y n * (x - y) = x ^ n - y ^ n

source

theorem geom_sum₂_mul {α : Type u} [comm_ring α] (x y : α) (n : ℕ) :

geom_series₂ x y n * (x - y) = x ^ n - y ^ n

source

theorem geom_sum_mul {α : Type u} [ring α] (x : α) (n : ℕ) :

geom_series x n * (x - 1) = x ^ n - 1

source

theorem mul_geom_sum {α : Type u} [ring α] (x : α) (n : ℕ) :

(x - 1) * geom_series x n = x ^ n - 1

source

theorem geom_sum_mul_neg {α : Type u} [ring α] (x : α) (n : ℕ) :

geom_series x n * (1 - x) = 1 - x ^ n

source

theorem mul_neg_geom_sum {α : Type u} [ring α] (x : α) (n : ℕ) :

(1 - x) * geom_series x n = 1 - x ^ n

source

theorem geom_sum {α : Type u} [division_ring α] {x : α} (h : x ≠ 1) (n : ℕ) :

geom_series x n = (x ^ n - 1) / (x - 1)

source

theorem geom_sum_Ico_mul {α : Type u} [ring α] (x : α) {m n : ℕ} :

m ≤ n → (finset.Ico m n).sum (λ (i : ℕ), x ^ i) * (x - 1) = x ^ n - x ^ m

source

theorem geom_sum_Ico_mul_neg {α : Type u} [ring α] (x : α) {m n : ℕ} :

m ≤ n → (finset.Ico m n).sum (λ (i : ℕ), x ^ i) * (1 - x) = x ^ m - x ^ n

source

theorem geom_sum_Ico {α : Type u} [division_ring α] {x : α} (hx : x ≠ 1) {m n : ℕ} :

m ≤ n → (finset.Ico m n).sum (λ (i : ℕ), x ^ i) = (x ^ n - x ^ m) / (x - 1)

source

theorem geom_sum_inv {α : Type u} [division_ring α] {x : α} (hx1 : x ≠ 1) (hx0 : x ≠ 0) (n : ℕ) :

geom_series x⁻¹ n = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)

source

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

source

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

mathlib documentation

algebra.geom_sum

General documentation

Additional documentation

Library

mathlib documentation

algebra.​geom_sum

General documentation

Additional documentation

Library

algebra.geom_sum