pderiv_mul — Mathlib

English

The derivative of a product satisfies the Leibniz rule: pderiv i (f g) = pderiv i f · g + f · pderiv i g.

Русский

Производная произведения удовлетворяет правилу Лейбница: ∂_i(fg) = (∂_i f) g + f (∂_i g).

LaTeX

$$$$ pderiv(i)(f g) = pderiv(i) f \\cdot g + f \\cdot pderiv(i) g. $$$$

Lean4

theorem pderiv_mul {i : σ} {f g : MvPolynomial σ R} : pderiv i (f * g) = pderiv i f * g + f * pderiv i g := by
  simp only [(pderiv i).leibniz f g, smul_eq_mul, mul_comm, add_comm]

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