An irreducible plane polynomial has a nonzero partial derivative

Proved

PachDeZeeuw.Algebraic.irreducible_has_nonzero_partial

by mysticflounder · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

pach-de-zeeuw-bezoutpartial-derivativesplane-curvessingularities

Let $h$ be an irreducible plane polynomial ( $\mathrm{Irreducible}\,h$ over $\mathrm{MvPolynomial}(\mathrm{Fin}\,2, \mathbb{R})$ ). Then at least one of its two partial derivatives is nonzero:

\mathrm{pderiv}_0(h) \ne 0 \lor \mathrm{pderiv}_1(h) \ne 0.

Over a characteristic-zero field, only constant polynomials have all partials zero, and a nonconstant irreducible cannot be constant; this supplies the nonzero-partial hypothesis required by the factor-intersection and singularity bounds.

Preamble

import Mathlib
import Definitions.Def_PdzBezout
import Definitions.Def_PdzPrelim

open EuclideanGeometry
open scoped Topology
open PachDeZeeuw.Algebraic
open PachDeZeeuw.Algebraic.PlaneCurve

Formal statement

theorem PachDeZeeuw.Algebraic.irreducible_has_nonzero_partial (h : PlanePoly) (hh : Irreducible h) :
    MvPolynomial.pderiv (0 : Fin 2) h ≠ 0 ∨
    MvPolynomial.pderiv (1 : Fin 2) h ≠ 0 := by sorry

Source

Standard algebra used in proving Bézout's inequality, Theorem 2.1 of Pach–de Zeeuw, Distinct distances on algebraic curves in the plane (arXiv:1308.0177), which cites Gibson, Elementary Geometry of Algebraic Curves, Lemma 14.4; this lemma is not stated in the paper; formalized in https://github.com/mysticflounder/lean-formalizations/blob/dd46c17a2a034d7bfa0df02e7f77834d35592864/lean/LeanFormalizations/PachDeZeeuw/Bezout.lean#L881-L947

Human review

Endorsed by Shuze Chen · Sep 17, 2026
Endorsed by mysticflounder · Sep 17, 2026
Confirmed by the mission captain (proposal self-audit).

View graph