Executable dense-polynomial remainder agrees with Mathlib polynomial remainder over every field.
The executable long-division laws are valid over every Mathlib field. The low priority lets coefficient libraries retain specialized proof packages without creating an instance-selection preference cycle.
Executable dense-polynomial gcd and xgcd laws over every Mathlib field.
The raw executable dense-polynomial gcd is associated to Mathlib's normalized
polynomial gcd under toPolynomial. It is not generally equal before normalization:
Hex.DensePoly.gcd returns the last Euclidean remainder, while
EuclideanDomain.gcd for polynomials over a field is normalized.
The raw gcd component of Hex.DensePoly.xgcd is associated to Mathlib's
normalized polynomial gcd. This is the xgcd-facing form of
toPolynomial_gcd_associated, not a literal equality of raw outputs.
The executable Bezout identity transports across toPolynomial.
The right hand side is the executable raw gcd component, not Mathlib's
normalized polynomial gcd. The @[simp] direction collapses the transported
Bezout combination to the named raw gcd; the matching pattern only fires when
the goal mentions Hex.DensePoly.xgcd p q literally with both coefficient
projections, so the rule is narrow.
The transported executable Bezout combination is associated to Mathlib's normalized polynomial gcd. This is the normalization-aware xgcd correspondence surface: executable coefficients certify the raw gcd, whose transport is associated to Mathlib's canonical gcd.
The ring equivalence sends the executable raw gcd to a polynomial associated to Mathlib's normalized gcd. Use this theorem when the caller only needs the gcd universal property; do not assume raw executable gcd outputs are normalized.
The ring-equivalence form of the normalization-aware xgcd correspondence: the executable Bezout combination is associated to Mathlib's normalized gcd.