A Laurent-series derivative has zero residue

Proved

OAI.PiExponent.laurent_derivative_residue_eq_zero

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

differential-algebranumber-theoryopenai-pi-exponent-017

For any field $K$ and formal Laurent series $f$ over $K$ , the coefficient of $X^{-1}$ in its formal derivative is zero. This is the residue obstruction to a Laurent series being a derivative.

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_residue_eq_zero {K : Type*} [Field K]
    (f : K⸨X⸩) : (LaurentSeries.derivative K f).coeff (-1) = 0 := by sorry

Source

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

View graph