Discriminants under affine substitution

The resultant formula follows from the permutation of roots under the affine map. Applying it to a polynomial and its derivative gives equation (38), including degrees zero and one.

theorem NairTenenbaum.resultant_comp_linear_of_splits {K : Type u_1} [Field K] (f g : Polynomial K) (n : ℕ) (hg : g.natDegree ≤ n) (hf : f.Splits) (a b : K) (ha : a ≠ 0) : (f.comp (Polynomial.C a * Polynomial.X + Polynomial.C b)).resultant (g.comp (Polynomial.C a * Polynomial.X + Polynomial.C b)) f.natDegree n = a ^ (f.natDegree * n) * f.resultant g f.natDegree n

Simultaneous affine substitution in a resultant over a splitting field.

theorem NairTenenbaum.resultant_comp_affine (f g : Polynomial ℤ) (n : ℕ) (hg : g.natDegree ≤ n) (q : ℕ) (a : ℤ) (hq : q ≠ 0) : (f.comp (affinePolynomial q a)).resultant (g.comp (affinePolynomial q a)) f.natDegree n = ↑q ^ (f.natDegree * n) * f.resultant g f.natDegree n

The integral resultant identity, transported through the complex numbers. The bound on the second degree permits applying this with the derivative.

theorem NairTenenbaum.discr_comp_affine (f : Polynomial ℤ) (q : ℕ) (a : ℤ) (hq : q ≠ 0) : (f.comp (affinePolynomial q a)).discr = ↑q ^ (f.natDegree * (f.natDegree - 1)) * f.discr

Equation (38), for every integral polynomial and every nonzero natural slope. No monicity or separability hypothesis is required.