theorem Hex.DensePoly.eval_resultant {R : Type u} [CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] (f g : DensePoly (DensePoly R)) (a : R) : (f.resultant g).eval a = (f.specialize a).resultant (g.specialize a) f.natDegree g.natDegree

Specializing the coefficient variable after elimination agrees with the formal-degree Mathlib resultant of the specialized inputs.

theorem Hex.DensePoly.resultant_eq_zero_of_common_eval {R : Type u} [CommRing R] [IsDomain R] (F G : Polynomial R) (b : R) (hF : Polynomial.eval b F = 0) (hG : Polynomial.eval b G = 0) (hne : F ≠ 0 ∨ G ≠ 0) : F.resultant G = 0

Over a domain, a common root makes the default-degree resultant vanish as soon as at least one polynomial is nonzero. The proof maps injectively to the fraction field and uses Mathlib's field criterion.

theorem Hex.DensePoly.eval_resultant_default {R : Type u} [CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] (f g : DensePoly (DensePoly R)) (a : R) (hf : f.leadingCoeff.eval a ≠ 0) (hg : g.leadingCoeff.eval a ≠ 0) : (f.resultant g).eval a = (f.specialize a).resultant (g.specialize a)

The specialization law at default Mathlib degrees when neither outer leading coefficient vanishes.

theorem Hex.DensePoly.eval_resultant_eq_zero_of_common_root {R : Type u} [CommRing R] [IsDomain R] [DecidableEq R] [Div R] [ExactDivLaws R] (f g : DensePoly (DensePoly R)) (a b : R) (hpos : 1 < f.size ∨ 1 < g.size) (hfb : f.evalBivariate a b = 0) (hgb : g.evalBivariate a b = 0) : (f.resultant g).eval a = 0

A common bivariate zero forces the specialized eliminant to vanish when at least one input genuinely has positive degree in the eliminated variable. The condition excludes the formal-degree (0, 0) resultant, whose value is 1.