sum_balance — Mathlib

English

Let f be a function from a finite index set ι into an additive group G with a compatible ℚ≥0–module structure. Then the sum over all x of balance f(x) equals 0.

Русский

Пусть f : ι → G, где ι конечен, G — аддитивная абелева группа с модулем над ℚ≥0. Тогда сумма по x баланса balance f(x) равна нулю.

LaTeX

$$$$ \\sum_{x \\in \\mathrm{univ}} \\mathrm{balance}(f)(x) = 0. $$$$

Lean4

@[simp]
theorem sum_balance (f : ι → G) : ∑ x, balance f x = 0 := by cases isEmpty_or_nonempty ι <;> simp [balance_apply]

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