feat: add some simple results regarding polynomials (#10572)

- `Polynomial.map_contract`: `Polynomial.map` and `Polynomial.contract` commutes
- `Irreducible.natDegree_pos`: an irreducible polynomial over a field must have positive degree (not true if it's not a field)
- `Polynomial.Monic.nextCoeff_pow`: corollary of `Polynomial.Monic.nextCoeff_mul`
- `Polynomial.exists_monic_irreducible_factor`: a polynomial over a field which is not a unit must have a monic irreducible factor (not true if it's not a field)

Author: acmepjz

Mathlib/Data/Polynomial/Expand.lean

@@ -221,6 +221,10 @@ theorem coeff_contract {p : ℕ} (hp : p ≠ 0) (f : R[X]) (n : ℕ) :
     _ ≤ n * p := mul_le_mul_of_nonneg_left (show 1 ≤ p from hp.bot_lt) (zero_le n)
 #align polynomial.coeff_contract Polynomial.coeff_contract
 
+theorem map_contract {p : ℕ} (hp : p ≠ 0) {f : R →+* S} {q : R[X]} :
+    (q.contract p).map f = (q.map f).contract p := ext fun n ↦ by
+  simp only [coeff_map, coeff_contract hp]
+
 theorem contract_expand {f : R[X]} (hp : p ≠ 0) : contract p (expand R p f) = f := by
   ext
   simp [coeff_contract hp, coeff_expand hp.bot_lt, Nat.mul_div_cancel _ hp.bot_lt]

Mathlib/Data/Polynomial/FieldDivision.lean

@@ -676,3 +676,11 @@ theorem irreducible_iff_lt_natDegree_lt {p : R[X]} (hp0 : p ≠ 0) (hpu : ¬ IsU
 end Field
 
 end Polynomial
+
+/-- An irreducible polynomial over a field must have positive degree. -/
+theorem Irreducible.natDegree_pos {F : Type*} [Field F] {f : F[X]} (h : Irreducible f) :
+    0 < f.natDegree := Nat.pos_of_ne_zero fun H ↦ by
+  obtain ⟨x, hf⟩ := natDegree_eq_zero.1 H
+  by_cases hx : x = 0
+  · rw [← hf, hx, map_zero] at h; exact not_irreducible_zero h
+  exact h.1 (hf ▸ isUnit_C.2 (Ne.isUnit hx))

Mathlib/Data/Polynomial/Monic.lean

@@ -215,6 +215,11 @@ theorem nextCoeff_mul (hp : Monic p) (hq : Monic q) :
       show Nat.succ 0 = 1 from rfl]
 #align polynomial.monic.next_coeff_mul Polynomial.Monic.nextCoeff_mul
 
+theorem nextCoeff_pow (hp : p.Monic) (n : ℕ) : (p ^ n).nextCoeff = n • p.nextCoeff := by
+  induction n with
+  | zero => rw [pow_zero, Nat.zero_eq, zero_smul, ← map_one (f := C), nextCoeff_C_eq_zero]
+  | succ n ih => rw [pow_succ, hp.nextCoeff_mul (hp.pow n), ih, succ_nsmul]
+
 theorem eq_one_of_map_eq_one {S : Type*} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : p.Monic)
     (map_eq : p.map f = 1) : p = 1 := by
   nontriviality R

Mathlib/RingTheory/Polynomial/Basic.lean

@@ -1339,3 +1339,14 @@ instance (priority := 100) uniqueFactorizationMonoid :
 end MvPolynomial
 
 end UniqueFactorizationDomain
+
+/-- A polynomial over a field which is not a unit must have a monic irreducible factor.
+See also `WfDvdMonoid.exists_irreducible_factor`. -/
+theorem Polynomial.exists_monic_irreducible_factor {F : Type*} [Field F] (f : F[X])
+    (hu : ¬IsUnit f) : ∃ g : F[X], g.Monic ∧ Irreducible g ∧ g ∣ f := by
+  by_cases hf : f = 0
+  · exact ⟨X, monic_X, irreducible_X, hf ▸ dvd_zero X⟩
+  obtain ⟨g, hi, hf⟩ := WfDvdMonoid.exists_irreducible_factor hu hf
+  have ha : Associated g (g * C g.leadingCoeff⁻¹) := associated_mul_unit_right _ _ <|
+    isUnit_C.2 (leadingCoeff_ne_zero.2 hi.ne_zero).isUnit.inv
+  exact ⟨_, monic_mul_leadingCoeff_inv hi.ne_zero, ha.irreducible hi, ha.dvd_iff_dvd_left.1 hf⟩