zero_geom_sum — Mathlib

English

Sum of 0^i over range n equals the same expression as in Geom Sum Zero (specialized to 0).

Русский

Сумма 0^i по диапазону n равна выражению, аналогичному нулевой геометрической сумме (для 0).

LaTeX

$$$\\sum_{i=0}^{n-1} 0^{i} = \\begin{cases}0,& n=0\\\\ 1,& n>0\\end{cases}$$$

Lean4

@[simp]
theorem zero_geom_sum : ∀ {n}, ∑ i ∈ range n, (0 : R) ^ i = if n = 0 then 0 else 1
  | 0 => by simp
  | 1 => by simp
  | n + 2 => by
    rw [geom_sum_succ']
    simp [zero_geom_sum]

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