English
Value of a geometric sum: for m ≥ 2, ∑_{k=0}^{n-1} m^k = (m^n − 1)/(m − 1).
Русский
Значение геометрической суммы: при m ≥ 2 верно ∑_{k=0}^{n-1} m^k = (m^n − 1)/(m − 1).
LaTeX
$$$$ \sum_{k=0}^{n-1} m^k = \frac{m^n - 1}{m - 1} \quad (2 \le m) $$$$
Lean4
/-- Value of a geometric sum over the naturals. Note: see `geom_sum_mul_add` for a formulation
that avoids division and subtraction. -/
theorem geomSum_eq (hm : 2 ≤ m) (n : ℕ) : ∑ k ∈ range n, m ^ k = (m ^ n - 1) / (m - 1) :=
by
refine (Nat.div_eq_of_eq_mul_left (tsub_pos_iff_lt.2 hm) <| tsub_eq_of_eq_add ?_).symm
simpa only [tsub_add_cancel_of_le (by cutsat : 1 ≤ m), eq_comm] using geom_sum_mul_add (m - 1) n
