24.7. A small exact computation
For f = X² - 2 and g = X - 3, the resultant is f(3) = 7; the
discriminant of f is 8. Both checks below run the Mathlib-free algorithm.
open Hex
namespace HexResultantChapter
private def f : DensePoly Int := DensePoly.ofList [-2, 0, 1]
private def g : DensePoly Int := DensePoly.ofList [-3, 1]
#guard DensePoly.resultant f g = 7
#guard DensePoly.disc f = 8
end HexResultantChapter