Specialization and resultant in one distinguished variable
DefinitionEsgk_MultivariateEliminationResultantalgebraelimination-theorypolynomials
This views a multivariate polynomial as a univariate polynomial over the remaining variables, specializes those variables to real values, and forms the resultant of two such polynomials.
Definition code
-- Extracted dependency interfaces and their necessary proofs.
import Mathlib
import Mathlib.Algebra.MvPolynomial.Equiv
import Mathlib.Data.Real.Basic
import Mathlib.RingTheory.Polynomial.Resultant.Basic
/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/
noncomputable section
namespace Esgk
def headCurry {n : ℕ} (p : MvPolynomial (Fin (n + 1)) ℝ) :
Polynomial (MvPolynomial (Fin n) ℝ) :=
MvPolynomial.finSuccEquiv ℝ n p
def specializeRemainingVariables {n : ℕ} (x : Fin n → ℝ)
(p : MvPolynomial (Fin (n + 1)) ℝ) :
Polynomial ℝ :=
(headCurry p).map (MvPolynomial.eval x)
def headResultant {n : ℕ} (p q : MvPolynomial (Fin (n + 1)) ℝ) :
MvPolynomial (Fin n) ℝ :=
Polynomial.resultant (headCurry p) (headCurry q)
end Esgk