English
The Leibniz rule holds for formal derivatives: derivative(f·g) = f·derivative(g) + g·derivative(f).
Русский
Правило Лейбница выполняется для формальных производных: (fg)' = f g' + g f'.
LaTeX
$$$ \\mathrm{derivative}(f g) = f \\cdot \\mathrm{derivative}(g) + g \\cdot \\mathrm{derivative}(f) $$$
Lean4
/-- **Leibniz rule for formal power series**. -/
theorem derivativeFun_mul (f g : R⟦X⟧) : derivativeFun (f * g) = f • g.derivativeFun + g • f.derivativeFun :=
by
ext n
have h₁ : n < n + 1 := lt_succ_self n
have h₂ : n < n + 1 + 1 := Nat.lt_add_right _ h₁
rw [coeff_derivativeFun, map_add, coeff_mul_eq_coeff_trunc_mul_trunc _ _ (lt_succ_self _), smul_eq_mul, smul_eq_mul,
coeff_mul_eq_coeff_trunc_mul_trunc₂ g f.derivativeFun h₂ h₁,
coeff_mul_eq_coeff_trunc_mul_trunc₂ f g.derivativeFun h₂ h₁, trunc_derivativeFun, trunc_derivativeFun, ← map_add, ←
derivativeFun_coe_mul_coe, coeff_derivativeFun]
