A simple pole is not regular
ProvedLiouvilleDiffAlg.ratFunc_residue_not_regdifferential-algebrasymbolic-integration
Let be a field and with irreducible and . Let be nonzero. Then the rational function has a genuine pole at : there are no polynomials with and in .
This says that a nonzero multiple of a function with a simple pole cannot be rewritten with a denominator coprime to .
Formalization Note The statement is purely algebraic; is viewed in via the canonical embedding.
Preamble
import Mathlib open scoped Differential open Polynomial
Formal statement
namespace LiouvilleDiffAlg
theorem ratFunc_residue_not_reg {K : Type*} [Field K] {p q : K[X]} (hp : Irreducible p)
(hpq : ¬ p ∣ q) {c : K} (hc : c ≠ 0) :
¬ ∃ a b : K[X], ¬ p ∣ b ∧ algebraMap K (RatFunc K) c * (algebraMap K[X] (RatFunc K) q / algebraMap K[X] (RatFunc K) p) * algebraMap K[X] (RatFunc K) b = algebraMap K[X] (RatFunc K) a := by sorry
end LiouvilleDiffAlg
Source
Rosenlicht, Integration in finite terms, Amer. Math. Monthly 79 (1972), 963–972 (proof of Liouville's theorem by induction on an elementary tower); Geddes–Czapor–Labahn, Algorithms for Computer Algebra (Kluwer, 1992), §12.4; Wikipedia, "Liouville's theorem (differential algebra)", oldid=1349223559, section "Basic theorem"