theorem Hex.DensePoly.toPolynomial_disc {R : Type u} [CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] (f : DensePoly R) : f.disc = (HexPolyMathlib.toPolynomial f).discr

The executable and Mathlib discriminants agree under dense-polynomial correspondence.

theorem Hex.DensePoly.disc_mul {R : Type u} [CommRing R] [IsDomain R] [IsAddTorsionFree R] [DecidableEq R] [Div R] [ExactDivLaws R] (f g : DensePoly R) (hf : 0 < f.natDegree) (hg : 0 < g.natDegree) : (f * g).disc = f.disc * g.disc * f.resultant g ^ 2

Discriminants multiply with the square of the cross-resultant.

The positive-degree hypotheses are essential: Mathlib and the executable API assign discriminant one to constants, while multiplying by a nonunit constant scales the other discriminant.

theorem Hex.DensePoly.disc_ne_zero_iff_separable {R : Type u} [Field R] [IsAddTorsionFree R] [DecidableEq R] [ExactDivLaws R] (f : DensePoly R) (hf : 0 < f.natDegree) : f.disc ≠ 0 ↔ (HexPolyMathlib.toPolynomial f).Separable

A positive-degree polynomial over a characteristic-zero field has nonzero executable discriminant exactly when it is separable.