geom_sum_mul_of_one_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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