eval_multiset_prod_X_sub_C_derivative

English

Same as derivative_sub: derivative of a difference is the difference of derivatives.

Русский

То же самое что и производная разности: производная разности равна разности производных.

LaTeX

$$$\operatorname{derivative}(f - g) = \operatorname{derivative}(f) - \operatorname{derivative}(g)$$$

Lean4

theorem eval_multiset_prod_X_sub_C_derivative [DecidableEq R] {S : Multiset R} {r : R} (hr : r ∈ S) :
    eval r (derivative (Multiset.map (fun a => X - C a) S).prod) = (Multiset.map (fun a => r - a) (S.erase r)).prod :=
  by
  nth_rw 1 [← Multiset.cons_erase hr]
  have := (evalRingHom r).map_multiset_prod (Multiset.map (fun a => X - C a) (S.erase r))
  simpa using this

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