English
Let s be a finite index set and f: ι → R[X]. The derivative distributes over finite sums: the derivative of the sum over b in s of f(b) equals the sum over b in s of the derivative of f(b).
Русский
Пусть s — конечное множество индексов и f: ι → R[X]. Производная распределяется по конечной сумме: производная от суммы по b∈s f(b) равна суммы производных от f(b).
LaTeX
$$$\operatorname{derivative}\left(\sum_{b \in s} f(b)\right) = \sum_{b \in s} \operatorname{derivative}(f(b))$$$
Lean4
theorem derivative_sum {s : Finset ι} {f : ι → R[X]} : derivative (∑ b ∈ s, f b) = ∑ b ∈ s, derivative (f b) :=
map_sum ..