English
Let R and S be semirings and p be a polynomial in R[X]. For every ring homomorphism f : R →+* S, the sumIDeriv operator commutes with the map operation, i.e. sumIDeriv(p.map f) = (sumIDeriv p).map f.
Русский
Пусть R и S — полукольца и p — многочлен над R. Для любого кольцевого гомоморфа f : R →+* S выполняется равенство sumIDeriv(p.map f) = (sumIDeriv p).map f.
LaTeX
$$$$ \operatorname{sumIDeriv}(p.map\ f) = (\operatorname{sumIDeriv} p).map\ f $$$$
Lean4
@[simp]
theorem sumIDeriv_map (p : R[X]) (f : R →+* S) : sumIDeriv (p.map f) = (sumIDeriv p).map f :=
by
let n := max (p.map f).natDegree p.natDegree
rw [sumIDeriv_apply_of_le (le_max_left _ _ : _ ≤ n)]
rw [sumIDeriv_apply_of_le (le_max_right _ _ : _ ≤ n)]
simp_rw [Polynomial.map_sum, iterate_derivative_map p f]
