English
Let A be a commutative ring with a differential; let R be a commutative ring with a differential and an A-algebra structure A → R, together with a differential algebra structure. For x ∈ R and a polynomial v ∈ A[X], if the derivative of x satisfies x' = aeval_x(v) for some aeval homomorphism aeval_x, then for every p ∈ A[X], the derivative of aeval_x(p) equals aeval_x(implicitDeriv(v, p)).
Русский
Пусть A — коммутативное кольцо с производной; R — коммутативное кольцо с производной, оснащённое структурой A-алгебры. Для x ∈ R и полинома v ∈ A[X], если производная x удовлетворяет x' = aeval_x(v), то для каждого p ∈ A[X] производная от aeval_x(p) равна aeval_x(implicitDeriv(v, p)).
LaTeX
$$$\forall \{A : Type\*\} \{R : Type\*\} [\mathrm{CommRing} A] [\mathrm{Differential } A] [\mathrm{CommRing} R] [\mathrm{Differential } R] [Algebra A R] \, (x : R) \,(v : A[X]) \,(p : A[X]) \, , \, (x') = \mathrm{aeval}_x(v) \Rightarrow (\mathrm{aeval}_x(p))' = \mathrm{aeval}_x(\mathrm{implicitDeriv}(v,p)).$$$
Lean4
theorem deriv_aeval_eq_implicitDeriv (x : R) (v : A[X]) (h : x′ = aeval x v) (p : A[X]) :
(aeval x p)′ = aeval x (implicitDeriv v p) := by simp [deriv_aeval_eq, implicitDeriv, h, mul_comm]
