derivative_sum — Mathlib

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 ..

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