sum_map_div — Mathlib

English

For a division semiring K, a finite multiset s, a function f, and a scalar a ≠ 0, the sum of f(x)/a over x in s equals (sum of f over s) divided by a.

Русский

В кольце делимости сумма по мультимножеству функций делится на a пропорционально, то есть sum f(x)/a = (sum f(x))/a.

LaTeX

$$$$\\sum_{i\\in s} \\frac{f(i)}{a} = \\frac{1}{a} \\sum_{i\\in s} f(i)$$$$

Lean4

theorem sum_map_div (s : Multiset ι) (f : ι → K) (a : K) : (s.map (fun x ↦ f x / a)).sum = (s.map f).sum / a := by
  simp only [div_eq_mul_inv, Multiset.sum_map_mul_right]

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