Factorization of monic polynomials of given degree

This file contains two main results:

• Polynomial.IsMonicOfDegree.eq_mul_isMonicOfDegree_one_isMonicOfDegree shows that a monic polynomial of positive degree over an algebraically closed field can be written as a monic polynomial of degree 1 times another monic factor.

• Polynomial.IsMonicOfDegree.eq_mul_isMonicOfDegree_two_isMonicOfDegree shows that a monic polynomial of degree at least two over ℝ can be written as a monic polynomial of degree two times another monic factor.

theorem Polynomial.IsMonicOfDegree.eq_isMonicOfDegree_one_mul_isMonicOfDegree {F : Type u_1} [Field F] [IsAlgClosed F] {f : Polynomial F} {n : ℕ} (hf : f.IsMonicOfDegree (n + 1)) : ∃ (f₁ : Polynomial F) (f₂ : Polynomial F), f₁.IsMonicOfDegree 1 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

If f : F[X] is monic of degree ≥ 1 and F is an algebraically closed field, then f = f₁ * f₂ with f₁ monic of degree 1 and f₂ monic of degree f.natDegree - 1.

theorem Polynomial.IsMonicOfDegree.eq_isMonicOfDegree_one_or_two_mul {f : Polynomial ℝ} {n : ℕ} (hf : f.IsMonicOfDegree (n + 1)) : ∃ (f₁ : Polynomial ℝ) (f₂ : Polynomial ℝ), (f₁.IsMonicOfDegree 1 ∨ f₁.IsMonicOfDegree 2) ∧ f = f₁ * f₂

If f : ℝ[X] is monic of positive degree, then f = f₁ * f₂ with f₁ monic of degree 1 or 2.

This relies on the fact that irreducible polynomials over ℝ have degree at most 2.

theorem Polynomial.IsMonicOfDegree.eq_isMonicOfDegree_two_mul_isMonicOfDegree {f : Polynomial ℝ} {n : ℕ} (hf : f.IsMonicOfDegree (n + 2)) : ∃ (f₁ : Polynomial ℝ) (f₂ : Polynomial ℝ), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

If f : ℝ[X] is monic of degree ≥ 2, then f = f₁ * f₂ with f₁ monic of degree 2 and f₂ monic of degree f.natDegree - 2.

This relies on the fact that irreducible polynomials over ℝ have degree at most 2.