Prove2Me

The constants Con⁡(F)\operatorname{Con}(F) form a subfield

Proved
LiouvilleDiffAlg.constants_isSubfield

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

differential-algebra

Let FF be a differential field with derivation DD. Then the set of constants

Con⁡(F)={f∈F:Df=0}\operatorname{Con}(F) = \{ f \in F : Df = 0 \}

is a subfield of FF. It contains 00 and 11 and is closed under addition, negation, multiplication and inversion.

This justifies calling Con⁡(F)\operatorname{Con}(F) the field of constants of FF. It is used throughout the mission.

Preamble
import Mathlib
import Definitions.Def_LiouvilleDiffAlg_Basic

open scoped Differential
Formal statement
namespace LiouvilleDiffAlg

theorem constants_isSubfield (F : Type*) [Field F] [Differential F] :
    ∃ S : Subfield F, (S : Set F) = constants F := 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 "Definitions": "the constants of FF is the subfield Con⁡(F)={f∈F:Df=0}\operatorname{Con}(F)=\{f\in F : Df = 0\}"
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.

For every field FF equipped with a derivation DD (over Z\mathbb{Z}), there exists a subfield SS of FF whose underlying set is exactly {f∈F:Df=0}\{f \in F : Df = 0\}. No characteristic or other assumption is made on FF.

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