geom_sum_mul_of_le_one — Mathlib

English

Let R be a commutative semiring with x ≤ 1. Then the geometric sum ∑_{i=0}^{n-1} x^i times (1 − x) equals 1 − x^n.

Русский

Пусть R — коммутативное полукольцо и x ≤ 1. Тогда сумма ∑_{i=0}^{n-1} x^i, умноженная на (1 − x), равна 1 − x^n.

LaTeX

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

Lean4

theorem geom_sum_mul_of_le_one (hx : x ≤ 1) (n : ℕ) : (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n := by
  simpa using geom_sum₂_mul_of_le hx n

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