English
For any ring R and natural m, the sum over n in Fin m of (-1)^n equals 0 if m is even and 1 if m is odd.
Русский
Для кольца R и натурального m сумма по n в Fin m от (-1)^n равна 0, если m чётно, и 1, если нечетно.
LaTeX
$$$$\\sum_{n \\in \\mathrm{Fin} m} (-1)^n = \\begin{cases}0, & \\text{if } m \\text{ is even} \\\\ 1, & \\text{if } m \\text{ is odd}.\\end{cases}$$$$
Lean4
theorem sum_neg_one_pow (R : Type*) [Ring R] (m : ℕ) : (∑ n : Fin m, (-1) ^ n.1 : R) = if Even m then 0 else 1 := by
induction m with
| zero => simp
| succ n
IH =>
simp only [Fin.sum_univ_castSucc, Fin.coe_castSucc, IH, Fin.val_last, Nat.even_add_one, ite_not]
split_ifs with h
· simp [*]
· simp [(Nat.not_even_iff_odd.mp h).neg_pow]
