Currying of an irreducible positive-degree plane polynomial is primitive
ProvedPachDeZeeuw.Algebraic.curry_isPrimitive_of_irreducible_positive_natDegreepach-de-zeeuw-bezoutplane-curvesprimitivityresultants
Let be an irreducible bivariate real polynomial () whose currying has positive degree, . Then the curried univariate polynomial over the coefficient ring is primitive:
Primitivity (content a unit) is the hypothesis needed for Gauss-type arguments: it allows coprimality over the coefficient ring to be transported to the fraction field, where the resultant nonvanishing argument runs.
Preamble
import Mathlib import Definitions.Def_PdzPrelim open EuclideanGeometry open scoped Topology open PachDeZeeuw.Algebraic open PachDeZeeuw.Algebraic.PlaneCurve
Formal statement
theorem PachDeZeeuw.Algebraic.curry_isPrimitive_of_irreducible_positive_natDegree (h : MvPolynomial (Fin 2) ℝ)
(hh : Irreducible h)
(hpos : 0 < (Curry0 h).natDegree) :
(Curry0 h).IsPrimitive := 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/AlgebraicPrelim.lean#L1086-L1096
Human review
Confirmed by the mission captain (proposal self-audit).