$\mathbb{C}(x)$ has a unique standard derivation $d/dx$

Proved

LiouvilleDiffAlg.ratFunc_standardDerivation_existsUnique

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-algebrarational-functions

There is exactly one derivation $D$ on the field $\mathbb{C}(x)$ of complex rational functions such that

D(p) = p' \qquad \text{for all } p \in \mathbb{C}[x],

where $p'$ is the formal derivative of the polynomial $p$ .

This makes $\mathbb{C}(x)$ with $d/dx$ a well-defined differential field, the setting of all examples in the mission. It also shows that the examples, which assume a standard derivation, are not vacuous.

Preamble

import Mathlib
import Definitions.Def_LiouvilleDiffAlg_RatFunc

open scoped Differential

Formal statement

namespace LiouvilleDiffAlg

theorem ratFunc_standardDerivation_existsUnique :
    ∃! d : Differential (RatFunc ℂ), @IsStandardDerivation d := by sorry

end LiouvilleDiffAlg

Source

Wikipedia, "Liouville's theorem (differential algebra)", revision oldid=1349223559, https://en.wikipedia.org/w/index.php?title=Liouville%27s_theorem_(differential_algebra)&oldid=1349223559, section "Examples": "the field

\mathbb{C}(x)

of rational functions in a single variable has a derivation given by the standard derivative with respect to that variable"

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statements below (Aristotle, by Harmonic), with full knowledge of the source article and of the intended meaning. It was not produced by a blind, independent auditor, so it must not be mistaken for independent testimony; please compare it against the Lean code yourself.

There exists exactly one derivation $D$ (over $\mathbb{Z}$ ) on the field $\mathbb{C}(x)$ of complex rational functions such that $D(p) = p'$ for every polynomial $p \in \mathbb{C}[x]$ (formal derivative, polynomials viewed as rational functions). "Exactly one" means existence, plus: any two derivations with this property are equal as derivations.

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

C(x)\mathbb{C}(x)C(x) has a unique standard derivation d/dxd/dxd/dx

$\mathbb{C}(x)$ has a unique standard derivation $d/dx$