English
For a ∈ A and a derivation d, the identity d(aeval a f) = aeval a (derivative f) · d a holds for all f ∈ R[X].
Русский
Для любого a ∈ A и выводной d верно d(aeval a f) = aeval a (derivative f) · d a для любого f ∈ R[X].
LaTeX
$$$d(\\mathrm{aeval}(a,f)) = \\mathrm{aeval}(a, \\operatorname{derivative}(f)) \\cdot d a.$$$
Lean4
/-- A form of the chain rule: if `f` is a polynomial over `R`
and `d : A → M` is an `R`-derivation then for all `a : A` we have
$$ d(f(a)) = f' (a) d a. $$
The equation is in `M`. For the same equation in `Module.AEval R M a`,
see `Derivation.compAEval_eq`.
-/
theorem comp_aeval_eq (d : Derivation R A M) (f : R[X]) : d (aeval a f) = aeval a (derivative f) • d a :=
calc
_ = (AEval.of R M a).symm (d.compAEval a f) := rfl
_ = _ := by simp [-compAEval_apply, compAEval_eq]
