sum_eq_zero — Mathlib

English

The sum of the values of an odd function over a finite type is zero.

Русский

Сумма значений нечётной функции по конечному множество равна нулю.

LaTeX

$$$\\sum_{a \in \alpha} f(a) = 0$$$

Lean4

/-- The sum of the values of an odd function is 0. -/
theorem sum_eq_zero [Fintype α] [InvolutiveNeg α] {f : α → β} (hf : f.Odd) : ∑ a, f a = 0 := by
  simpa only [neg_eq_self ℕ, Finset.sum_neg_distrib, funext hf, Equiv.neg_apply] using Equiv.sum_comp (.neg α) f

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