English
For a fixed a ∈ A and any polynomial f ∈ R[X], the derivation d.compAEval a applied to f equals the derivative of f evaluated at a, acting on d a: d.compAEval a f = (derivative f) · AEval.of R M a (d a).
Русский
Для фиксированного a ∈ A и любого f ∈ R[X] выполняется d.compAEval a f = f' · AEval.of R M a (d a).
LaTeX
$$$d.\\mathrm{compAEval}(a)\\; f = \\operatorname{derivative}(f) \\;\\cdot\\; \\mathrm{AEval.of}\\ R\\; M\\ a\\bigl(d a\\bigr).$$$
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 the `R[X]`-module `Module.AEval R M a`.
For the same equation in `M`, see `Derivation.compAEval_eq`.
-/
theorem compAEval_eq (d : Derivation R A M) (f : R[X]) : d.compAEval a f = derivative f • (AEval.of R M a (d a)) :=
by
rw [← mkDerivation_apply]
congr
apply derivation_ext
simp
