mul_geom_sum — Mathlib

English

(x − 1) times the geometric sum equals x^n − 1; equivalently, the same as previous but viewed with sides swapped.

Русский

Произведение (x − 1) на геометрическую сумму равно x^n − 1; эквивалентно той же формуле, но со стороны умножения.

LaTeX

$$$\\displaystyle (x - 1)\\left(\\sum_{i=0}^{n-1} x^i\\right) = x^n - 1$$$

Lean4

theorem mul_geom_sum (x : R) (n : ℕ) : ((x - 1) * ∑ i ∈ range n, x ^ i) = x ^ n - 1 :=
  op_injective <| by simpa using geom_sum_mul (op x) n

Похожие утверждения