theorem Hex.DensePoly.resultant_eq_leadingCoeff_mul_prod_roots {K : Type u} [Field K] [IsAlgClosed K] (f g : Polynomial K) : f.resultant g = f.leadingCoeff ^ g.natDegree * (Multiset.map (fun (x : K) => Polynomial.eval x g) f.roots).prod

The resultant as the leading-coefficient power times evaluation over all roots of the first polynomial, counted with multiplicity.