English
In any ring R, the alternating geometric sum ∑_{i=0}^{n-1} (−1)^i equals 0 when n is even and equals 1 when n is odd.
Русский
В кольце R сумма ∑_{i=0}^{n-1} (−1)^i чередуется: она равна 0 при чётном n и равна 1 при нечётном n.
LaTeX
$$$\\displaystyle \\sum_{i=0}^{n-1} (-1)^i = \\begin{cases}0, & \\text{if } n \\text{ is even}, \\\\ 1, & \\text{if } n \\text{ is odd}.\\end{cases}$$$
Lean4
@[simp]
theorem neg_one_geom_sum {n : ℕ} : ∑ i ∈ range n, (-1 : R) ^ i = if Even n then 0 else 1 := by
induction n with
| zero => simp
| succ k hk =>
simp only [geom_sum_succ', Nat.even_add_one, hk]
split_ifs with h
· rw [h.neg_one_pow, add_zero]
· rw [(Nat.not_even_iff_odd.1 h).neg_one_pow, neg_add_cancel]
