theorem Hex.DensePoly.resultant_eq_zero_iff_common_root (f g : DensePoly ℤ) (hf : f ≠ 0) : f.resultant g = 0 ↔ ∃ (z : ℂ), (Polynomial.aeval z) (HexPolyMathlib.toPolynomial f) = 0 ∧ (Polynomial.aeval z) (HexPolyMathlib.toPolynomial g) = 0

If the first integer dense polynomial is nonzero, the executable resultant vanishes exactly when the two polynomials share a complex root.