geom_sum_mul_neg — Mathlib

English

For any ring R and x, (1 − x) times the sum ∑_{i=0}^{n-1} x^i equals 1 − x^n.

Русский

Для кольца R и x выполняется: (1 − x) сумма ∑ x^i от i=0 до n−1 равна 1 − x^n.

LaTeX

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

Lean4

theorem geom_sum_mul_neg (x : R) (n : ℕ) : (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n :=
  by
  have := congr_arg Neg.neg (geom_sum_mul x n)
  rw [neg_sub, ← mul_neg, neg_sub] at this
  exact this

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