Degrees and separability of the polynomial family

The degree identities and the nonvanishing of D* asserted in §2 are consequences of the factorization data, rather than additional assumptions on that data.

theorem NairTenenbaum.discr_ne_zero_of_separable_map {Q : Polynomial ℤ} (hQ : (Polynomial.map (Int.castRingHom ℚ) Q).Separable) : Q.discr ≠ 0

Separability over the rationals forces the integral discriminant to be nonzero.

theorem NairTenenbaum.PolynomialSystem.factor_ne_zero {k r : ℕ} (P : PolynomialSystem k r) (h : Fin r) : P.R h ≠ 0

theorem NairTenenbaum.PolynomialSystem.sign_ne_zero {k r : ℕ} (P : PolynomialSystem k r) (j : Fin k) : P.sign j ≠ 0

theorem NairTenenbaum.PolynomialSystem.polynomial_ne_zero {k r : ℕ} (P : PolynomialSystem k r) (j : Fin k) : P.Q j ≠ 0

theorem NairTenenbaum.PolynomialSystem.total_ne_zero {k r : ℕ} (P : PolynomialSystem k r) : P.total ≠ 0

theorem NairTenenbaum.PolynomialSystem.radical_ne_zero {k r : ℕ} (P : PolynomialSystem k r) : P.radical ≠ 0

theorem NairTenenbaum.PolynomialSystem.total_factorization {k r : ℕ} (P : PolynomialSystem k r) : P.total = Polynomial.C (∏ j : Fin k, P.sign j) * ∏ h : Fin r, P.R h ^ totalExponent P.exponent h

Collecting the exponents in the factorization of the total polynomial.

theorem NairTenenbaum.PolynomialSystem.total_sign_unit {k r : ℕ} (P : PolynomialSystem k r) : IsUnit (∏ j : Fin k, P.sign j)

theorem NairTenenbaum.PolynomialSystem.factor_dvd_total {k r : ℕ} (P : PolynomialSystem k r) (h : Fin r) : P.R h ∣ P.total

theorem NairTenenbaum.PolynomialSystem.factor_noFixedPrime {k r : ℕ} (P : PolynomialSystem k r) (h : Fin r) : NoFixedPrimeDivisor (P.R h)

theorem NairTenenbaum.PolynomialSystem.rootCount_total_eq_radical {k r : ℕ} (P : PolynomialSystem k r) {p : ℕ} (hp : Nat.Prime p) : rootCount P.total p = rootCount P.radical p

theorem NairTenenbaum.PolynomialSystem.radical_noFixedPrime {k r : ℕ} (P : PolynomialSystem k r) : NoFixedPrimeDivisor P.radical

theorem NairTenenbaum.PolynomialSystem.factor_degree_pos {k r : ℕ} (P : PolynomialSystem k r) (h : Fin r) : 0 < (P.R h).natDegree

theorem NairTenenbaum.PolynomialSystem.polynomial_degree {k r : ℕ} (P : PolynomialSystem k r) (j : Fin k) : (P.Q j).natDegree = ∑ h : Fin r, P.exponent j h * (P.R h).natDegree

theorem NairTenenbaum.PolynomialSystem.total_degree_eq_sum {k r : ℕ} (P : PolynomialSystem k r) : P.total.natDegree = ∑ j : Fin k, (P.Q j).natDegree

theorem NairTenenbaum.PolynomialSystem.total_degree {k r : ℕ} (P : PolynomialSystem k r) : P.total.natDegree = ∑ h : Fin r, totalExponent P.exponent h * (P.R h).natDegree

The degree identity g = ∑ γ_h r_h in §2.

theorem NairTenenbaum.PolynomialSystem.totalExponent_le_degree {k r : ℕ} (P : PolynomialSystem k r) (h : Fin r) : totalExponent P.exponent h ≤ P.total.natDegree

theorem NairTenenbaum.PolynomialSystem.radical_degree {k r : ℕ} (P : PolynomialSystem k r) : P.radical.natDegree = ∑ h : Fin r, (P.R h).natDegree

theorem NairTenenbaum.PolynomialSystem.radical_degree_le_total {k r : ℕ} (P : PolynomialSystem k r) : P.radical.natDegree ≤ P.total.natDegree

theorem NairTenenbaum.PolynomialSystem.factor_count_le_degree {k r : ℕ} (P : PolynomialSystem k r) : r ≤ P.total.natDegree

theorem NairTenenbaum.PolynomialSystem.factors_coprime {k r : ℕ} (P : PolynomialSystem k r) {i j : Fin r} (hij : i ≠ j) : IsCoprime (Polynomial.map (Int.castRingHom ℚ) (P.R i)) (Polynomial.map (Int.castRingHom ℚ) (P.R j))

theorem NairTenenbaum.PolynomialSystem.radical_separable {k r : ℕ} (P : PolynomialSystem k r) : (Polynomial.map (Int.castRingHom ℚ) P.radical).Separable

theorem NairTenenbaum.PolynomialSystem.discriminant_pos {k r : ℕ} (P : PolynomialSystem k r) : 0 < P.discriminant