Derivative of a polynomial in K(X)

Proved

LiouvilleDiffAlg.ratFunc_deriv_poly

by vebis · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-algebrasymbolic-integration

Assume $K$ is a field of characteristic zero with a derivation $D$ , and $K(X)$ is the field of rational functions in one variable over $K$ , equipped with a derivation (also written $D$ ) that extends the derivation of $K$ . Suppose $DX=w$ for a polynomial $w\in K[X]$ . Then for every polynomial $r\in K[X]$ ,

D r = r^{D} + w\,\frac{dr}{dX},

where $r^{D}\in K[X]$ denotes the polynomial obtained by applying $D$ to the coefficients of $r$ and $dr/dX$ is the formal derivative. In particular the derivative of a polynomial is again a polynomial.

This is the chain-rule formula that reduces differentiation in $K(X)$ to polynomial arithmetic.

Formalization Note The right-hand side is Differential.implicitDeriv w r.

Preamble

import Mathlib

open scoped Differential
open Polynomial

Formal statement

namespace LiouvilleDiffAlg

theorem ratFunc_deriv_poly {K : Type*} [Field K] [Differential K] [CharZero K]
    [Differential (RatFunc K)] [DifferentialAlgebra K (RatFunc K)]
    (w : K[X]) (hX : (RatFunc.X : RatFunc K)′ = algebraMap K[X] (RatFunc K) w) (r : K[X]) :
    (algebraMap K[X] (RatFunc K) r)′ = algebraMap K[X] (RatFunc K) (Differential.implicitDeriv w r) := by sorry

end LiouvilleDiffAlg

Source

Rosenlicht, Integration in finite terms, Amer. Math. Monthly 79 (1972), 963–972 (proof of Liouville's theorem by induction on an elementary tower); Geddes–Czapor–Labahn, Algorithms for Computer Algebra (Kluwer, 1992), §12.4; Wikipedia, "Liouville's theorem (differential algebra)", oldid=1349223559, section "Basic theorem"

View graph