$1/x$ has no antiderivative in $\mathbb{C}(x)$

Proved

LiouvilleDiffAlg.inv_X_no_antideriv

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$ . Then there is no rational function $g \in \mathbb{C}(x)$ with

Dg = \frac{1}{x}.

This is the basic example of an elementary function whose antiderivative requires a logarithmic extension.

Preamble

import Mathlib
import Definitions.Def_LiouvilleDiffAlg_RatFunc

open scoped Differential

Formal statement

namespace LiouvilleDiffAlg

theorem inv_X_no_antideriv [Differential (RatFunc ℂ)] (hD : IsStandardDerivation) :
    ¬ ∃ g : RatFunc ℂ, g′ = 1 / RatFunc.X := 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 function

f := 1/x

, which exists in

\mathbb{C}(x)

, does not have an antiderivative in

\mathbb{C}(x)

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$ . Then there is no $g \in \mathbb{C}(x)$ with $Dg = 1/x$ , where $x$ is the indeterminate viewed as a rational function (so $1/x$ is a genuine, nonzero rational function).

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

1/x1/x1/x has no antiderivative in C(x)\mathbb{C}(x)C(x)

$1/x$ has no antiderivative in $\mathbb{C}(x)$