The discriminant and simple residue roots

For a polynomial of degree at least two the discriminant belongs to the ideal generated by the polynomial and its derivative. The modified Sylvester matrix gives this without assuming that the leading coefficient is invertible.

theorem NairTenenbaum.exists_mul_add_mul_eq_C_discr {R : Type u_1} [CommRing R] (Q : Polynomial R) (hdeg : 2 ≤ Q.natDegree) : ∃ (U : Polynomial R) (V : Polynomial R), Q * U + Polynomial.derivative Q * V = Polynomial.C Q.discr

theorem NairTenenbaum.eval_derivative_ne_zero_of_degree_le_one {K : Type u_1} [Field K] {Q : Polynomial K} (hQ : Q ≠ 0) (hdeg : Q.natDegree ≤ 1) {a : K} (ha : Polynomial.eval a Q = 0) : Polynomial.eval a (Polynomial.derivative Q) ≠ 0

In degree at most one, a nonzero polynomial cannot have a multiple root.

theorem NairTenenbaum.discr_eq_one_of_natDegree_le_one {R : Type u_1} [CommRing R] {Q : Polynomial R} (hdeg : Q.natDegree ≤ 1) : Q.discr = 1

theorem NairTenenbaum.simple_roots_of_discr {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {p : ℕ} (hp : Nat.Prime p) (hD : ↑Q.discr ≠ 0) (a : ResidueRoots Q p) : Polynomial.eval₂ (Int.castRingHom (ZMod p)) (↑a) (Polynomial.derivative Q) ≠ 0

A prime not dividing the discriminant gives only simple residue roots. The no-fixed-prime condition also covers polynomials of degree zero or one.

theorem NairTenenbaum.simple_roots_of_dvd_discr {Q T : Polynomial ℤ} (hT : NoFixedPrimeDivisor T) (hQT : Q ∣ T) {p : ℕ} (hp : Nat.Prime p) (hD : ↑T.discr ≠ 0) (a : ResidueRoots Q p) : Polynomial.eval₂ (Int.castRingHom (ZMod p)) (↑a) (Polynomial.derivative Q) ≠ 0

theorem NairTenenbaum.rootCount_prime_pow_le_of_dvd_discr {Q T : Polynomial ℤ} (hT : NoFixedPrimeDivisor T) (hQT : Q ∣ T) {p ν : ℕ} (hp : Nat.Prime p) (hν : ν ≠ 0) (hD : ¬p ∣ T.discr.natAbs) : rootCount Q (p ^ ν) ≤ rootCount Q p

theorem NairTenenbaum.dvd_discr_of_dvd_eval_and_derivative {Q : Polynomial ℤ} (hdeg : 2 ≤ Q.natDegree) {d n : ℤ} (hQ : d ∣ Polynomial.eval n Q) (hQ' : d ∣ Polynomial.eval n (Polynomial.derivative Q)) : d ∣ Q.discr

Common divisors of the value and derivative divide the discriminant.

theorem NairTenenbaum.dvd_discr_of_dvd_two_factors {Q R S : Polynomial ℤ} (hdeg : 2 ≤ Q.natDegree) (hRS : R * S ∣ Q) {d n : ℤ} (hR : d ∣ Polynomial.eval n R) (hS : d ∣ Polynomial.eval n S) : d ∣ Q.discr

Two polynomial factors with a common value-divisor force that divisor into the discriminant of their product (or any polynomial divisible by the product).