English
Let K be a division semiring. For any finite index set s and any function f: s → K, and for any a ∈ K, the division distributes over summation: (∑ i∈s f(i)) / a = ∑ i∈s (f(i) / a).
Русский
Пусть K — делимый полукольцо. Для любого конечного множества индексов s и функции f: s → K и любого a ∈ K верно, что сумма делений по a распространяется на сумму: (∑ i∈s f(i)) / a = ∑ i∈s (f(i) / a).
LaTeX
$$$\left(\sum_{i \in s} f(i)\right)/a = \sum_{i \in s} \left( f(i)/a \right)$$$
Lean4
theorem sum_div (s : Finset ι) (f : ι → K) (a : K) : (∑ i ∈ s, f i) / a = ∑ i ∈ s, f i / a := by
simp only [div_eq_mul_inv, sum_mul]
-- TODO: Move these to `Algebra.BigOperators.Group.Finset.Basic`, next to the corresponding `card`
-- lemmas, once `Finset.dens` doesn't depend on `Field` anymore.
