English
For any polynomial p and ring hom f : R →+* S, derivative(p.map f) = (derivative p).map f.
Русский
Пусть p — многочлен над R, f — гомоморфизм колец R → S. Тогда производная от образа p через f равна образу от производной p через f.
LaTeX
$$$\operatorname{derivative}(p.map f) = (\operatorname{derivative}(p)).map f$$$
Lean4
@[simp]
theorem derivative_mul {f g : R[X]} : derivative (f * g) = derivative f * g + f * derivative g :=
by
induction f using Polynomial.induction_on' with
| add => simp only [add_mul, map_add, add_assoc, add_left_comm, *]
| monomial m a => ?_
induction g using Polynomial.induction_on' with
| add => simp only [mul_add, map_add, add_assoc, add_left_comm, *]
| monomial n b => ?_
simp only [monomial_mul_monomial, derivative_monomial]
simp only [mul_assoc, (Nat.cast_commute _ _).eq, Nat.cast_add, mul_add, map_add]
cases m with
| zero => simp only [zero_add, Nat.cast_zero, mul_zero, map_zero]
| succ m =>
cases n with
| zero => simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]
| succ n => grind
