Discriminants of products of nonmonic polynomials

The discriminant of a product of two positive-degree polynomials over a domain is the product of their discriminants and the square of their resultant. Unlike the monic product law, this applies to primitive polynomials over polynomial coefficient rings, where leading coefficients need not be units.

Positive degrees are essential with the convention Polynomial.discr_C = 1: multiplying by a constant instead obeys the scaling law TauCeti.discr_C_mul. Multiplying by X multiplies the discriminant by the square of the constant coefficient (Polynomial.discr_X_mul).

This extends Polynomial.Monic.discr_mul and supplies the discriminant identity for products of primitive basis members in McCallum projection, where the coefficient ring is a multivariate polynomial ring. Finset.map_discr_prod_eq packages its finite-product consequence for two multiplicative invariants agreeing on discriminants and pairwise resultants.

References

S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), Section 2 (discriminants and resultants of a polynomial basis).

theorem Polynomial.discr_mul_of_natDegree_pos {R : Type u} [CommRing R] [IsDomain R] (f g : Polynomial R) (hf : 0 < f.natDegree) (hg : 0 < g.natDegree) : (f * g).discr = f.discr * g.discr * f.resultant g ^ 2

The discriminant product law for positive-degree polynomials over an integral domain. No monicity, separability, or characteristic assumption is required.

theorem Polynomial.discr_X_mul {R : Type u} [CommRing R] [IsDomain R] (f : Polynomial R) (hf : 0 < f.natDegree) : (X * f).discr = f.discr * f.coeff 0 ^ 2

Multiplying a positive-degree polynomial over a domain by X multiplies its discriminant by the square of its constant coefficient.

theorem Finset.map_discr_prod_eq {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [IsDomain R] [CommMonoid M] (s : Finset ι) (f : ι → Polynomial R) (hdeg : ∀ i ∈ s, 0 < (f i).natDegree) (v w : R →* M) (hdiscr : ∀ i ∈ s, v (f i).discr = w (f i).discr) (hres : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → v ((f i).resultant (f j)) = w ((f i).resultant (f j))) : v (∏ i ∈ s, f i).discr = w (∏ i ∈ s, f i).discr

Two multiplicative invariants that agree on individual discriminants and pairwise resultants agree on the discriminant of the product. The factors have positive degree but need not be monic. Empty products and vanishing discriminants or resultants are included.