theorem Hex.SubresultantMinor.sign_eq_pow {R : Type u} [CommRing R] (j : ℕ) : sign j = (-1) ^ j

The parity sign used by the proof-only Laplace recursion is the usual power of -1.

theorem Hex.SubresultantMinor.det_eq_matrixDet {R : Type u} [CommRing R] {n : ℕ} (M : Square R n) : det M = (Matrix.of M).det

The dependency-free Laplace determinant used by hex-resultant agrees with Mathlib's determinant on the same finite square matrix.

theorem Hex.DensePoly.Subresultant.coeffMinorAt_zero_eq_resultant {R : Type u} [CommRing R] [DecidableEq R] (df dg : ℕ) (f g : DensePoly R) (hf : f.size ≤ df + 1) (hg : g.size ≤ dg + 1) : coeffMinorAt df dg 0 0 f g = (HexPolyMathlib.toPolynomial f).resultant (HexPolyMathlib.toPolynomial g) df dg

The zeroth generalized coefficient minor at explicit degree bounds is Mathlib's Sylvester determinant at those same bounds.

theorem Hex.DensePoly.Subresultant.coeffMinor_zero_eq_resultant {R : Type u} [CommRing R] [DecidableEq R] (f g : DensePoly R) : coeffMinor 0 0 f g = (HexPolyMathlib.toPolynomial f).resultant (HexPolyMathlib.toPolynomial g) (formalDegree f) (formalDegree g)

The zeroth generalized coefficient minor is Mathlib's Sylvester determinant at the same formal degrees.

theorem Hex.DensePoly.toPolynomial_resultant {R : Type u} [CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] (f g : DensePoly R) : f.resultant g = (HexPolyMathlib.toPolynomial f).resultant (HexPolyMathlib.toPolynomial g) f.natDegree g.natDegree

The executable and Mathlib resultants agree under dense-polynomial correspondence, with the executable default formal degrees made explicit.