sum_eq — Mathlib

English

For any natural n and d, the sum ∑_{i=0}^{n-1} d(2d+1)^i equals ((2d+1)^n − 1)/2.

Русский

Для любых натуральных n и d сумма ∑_{i=0}^{n-1} d(2d+1)^i равна ((2d+1)^n − 1)/2.

LaTeX

$$$ \\sum_{i=0}^{n-1} d(2d+1)^i = \\frac{(2d+1)^n - 1}{2} $$$

Lean4

theorem sum_eq : (∑ i : Fin n, d * (2 * d + 1) ^ (i : ℕ)) = ((2 * d + 1) ^ n - 1) / 2 :=
  by
  refine (Nat.div_eq_of_eq_mul_left zero_lt_two ?_).symm
  rw [← sum_range fun i => d * (2 * d + 1) ^ (i : ℕ), ← mul_sum, mul_right_comm, mul_comm d, ← geom_sum_mul_add,
    add_tsub_cancel_right, mul_comm]

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