mul_neg_geom_sum — Mathlib

English

For any ring R and x, ((1 − x) times the sum ∑ x^i) equals 1 − x^n, transported via opposite structure if needed.

Русский

Для кольца R и элемента x произведение (1 − x) на сумму ∑ x^i равно 1 − x^n (в нужной обёртке).

LaTeX

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

Lean4

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

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