$\operatorname{Con}(\mathbb{C}(x)) = \mathbb{C}$

Proved

LiouvilleDiffAlg.constants_ratFunc

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

differential-algebrarational-functions

Equip $\mathbb{C}(x)$ with the standard derivative $D = d/dx$ (any derivation with $D(p) = p'$ for all polynomials $p$ ). Then the constants are exactly the complex numbers:

\operatorname{Con}(\mathbb{C}(x)) = \{ r \in \mathbb{C}(x) : Dr = 0 \} = \mathbb{C}.

This identifies the constant field in the running example. It is the constant field that the hypothesis $\operatorname{Con}(F) = \operatorname{Con}(G)$ of Liouville's theorem refers to.

Preamble

import Mathlib
import Definitions.Def_LiouvilleDiffAlg_Basic
import Definitions.Def_LiouvilleDiffAlg_RatFunc

open scoped Differential

Formal statement

namespace LiouvilleDiffAlg

theorem constants_ratFunc [Differential (RatFunc ℂ)] (hD : IsStandardDerivation) :
    constants (RatFunc ℂ) = Set.range (algebraMap ℂ (RatFunc ℂ)) := 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 constants of this field are just the complex numbers

\mathbb{C}

; that is,

\operatorname{Con}(\mathbb{C}(x)) = \mathbb{C}

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.

Let $\mathbb{C}(x)$ carry a derivation $D$ (over $\mathbb{Z}$ ) with $D(p) = p'$ for every polynomial $p \in \mathbb{C}[x]$ . Then the set $\{r \in \mathbb{C}(x) : Dr = 0\}$ equals the set of constant rational functions, i.e. the image of $\mathbb{C}$ under its canonical embedding into $\mathbb{C}(x)$ .

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

Con⁡(C(x))=C\operatorname{Con}(\mathbb{C}(x)) = \mathbb{C}Con(C(x))=C

$\operatorname{Con}(\mathbb{C}(x)) = \mathbb{C}$