A Laurent-series derivative cannot be a nonzero simple pole

Proved

OAI.PiExponent.laurent_derivative_ne_simple_pole

by marwahaha · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-algebranumber-theoryopenai-pi-exponent-017

For any field $K$ , Laurent series $f$ over $K$ , and nonzero scalar $c\in K$ , the derivative of $f$ is not the Laurent monomial $cX^{-1}$ . The residue of a derivative vanishes, while the residue of this simple pole is $c$ .

Preamble

import Mathlib.Algebra.Polynomial.Derivation
import Mathlib.Algebra.Polynomial.Div
import Mathlib.RingTheory.LaurentSeries
import Mathlib.RingTheory.Trace.Defs
import Mathlib.Tactic


namespace OAI
namespace PiExponent
end PiExponent
end OAI
open scoped LaurentSeries Matrix
open OAI.PiExponent

Formal statement

theorem OAI.PiExponent.laurent_derivative_ne_simple_pole {K : Type*} [Field K]
    (f : K⸨X⸩) {c : K} (hc : c ≠ 0) :
    LaurentSeries.derivative K f ≠ HahnSeries.single (-1) c := by sorry

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Analysis/LogarithmicObstruction.lean#L19-L24

View graph