English
For a finite product of polynomials indexed by a multiset s, the derivative of the product equals the sum over i in s of (the product over j ≠ i of f_j) times f_i'.
Русский
Для конечного произведения многочленов, индексируемого мультисетом s, производная произведения равна сумме по i ∈ s от (произведение по j ≠ i f_j) умноженного на f_i'.
LaTeX
$$$\frac{d}{dX}\Big(\prod_{i \in s} f_i\Big) \,=\, \sum_{i \in s} \Big( \Big(\prod_{j \in s \setminus \{i\}} f_j\Big) \cdot f_i' \Big)$$$
Lean4
theorem derivative_prod [DecidableEq ι] {s : Multiset ι} {f : ι → R[X]} :
derivative (Multiset.map f s).prod =
(Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum :=
by
refine Multiset.induction_on s (by simp) fun i s h => ?_
rw [Multiset.map_cons, Multiset.prod_cons, derivative_mul, Multiset.map_cons _ i s, Multiset.sum_cons,
Multiset.erase_cons_head, mul_comm (derivative (f i))]
congr
rw [h, ← AddMonoidHom.coe_mulLeft, (AddMonoidHom.mulLeft (f i)).map_multiset_sum _, AddMonoidHom.coe_mulLeft]
simp only [Function.comp_apply, Multiset.map_map]
refine congr_arg _ (Multiset.map_congr rfl fun j hj => ?_)
rw [← mul_assoc, ← Multiset.prod_cons, ← Multiset.map_cons]
by_cases hij : i = j
· simp [hij, Multiset.cons_erase hj]
· simp [hij]
