Currys of nonassociated irreducibles are relatively prime

Proved

PachDeZeeuw.Algebraic.curry_isRelPrime_of_nonassociated_irreducibles

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

coprimalitypach-de-zeeuw-bezoutplane-curvesresultants

Let $h$ and $k$ be irreducible bivariate real polynomials that are not associated ( $\neg\,\mathrm{Associated}\,h\,k$ , i.e. they do not differ by a unit factor). Then their currys are relatively prime as univariate polynomials over the coefficient ring:

\mathrm{IsRelPrime}(\mathrm{Curry}_0(h),\, \mathrm{Curry}_0(k)).

This converts the geometric hypothesis 'distinct irreducible curves' into the algebraic coprimality hypothesis required for the resultant to be nonzero, and hence for the pair-intersection bound.

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_isRelPrime_of_nonassociated_irreducibles (h k : MvPolynomial (Fin 2) ℝ)
    (hh : Irreducible h) (hk : Irreducible k)
    (hnot : ¬ Associated h k) :
    IsRelPrime (Curry0 h) (Curry0 k) := 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#L1098-L1112

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