English
Let f ∈ ℝ[X] be monic with degree at least 2. Then there exist monic polynomials f1, f2 with deg f1 = 2 and deg f2 = deg f − 2 such that f = f1 f2.
Русский
Пусть f ∈ ℝ[X] является мономическим по степени и deg f ≥ 2. Тогда существуют мономические многочлены f1, f2 такие, что deg f1 = 2, deg f2 = deg f − 2 и f = f1 f2.
LaTeX
$$$$\\exists f_1,f_2 \\in \\mathbb{R}[X],\\; \\deg f_1 = 2 \\;\\land\\; \\deg f_2 = \\deg f - 2 \\;\\land\\; f_1 \\text{ и } f_2 \\text{ мономиальны} \\land f = f_1 f_2.$$$$
Lean4
/-- 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`. -/
-- TODO: generalize to real closed fields when they are available.
theorem eq_isMonicOfDegree_two_mul_isMonicOfDegree {f : ℝ[X]} {n : ℕ} (hf : IsMonicOfDegree f (n + 2)) :
∃ f₁ f₂ : ℝ[X], IsMonicOfDegree f₁ 2 ∧ IsMonicOfDegree f₂ n ∧ f = f₁ * f₂ :=
by
obtain ⟨g₁, g₂, hd₁ | hd₂, h⟩ := hf.eq_isMonicOfDegree_one_or_two_mul
all_goals rw [h, add_comm] at hf
· have hg₂ := of_mul_left hd₁ <| (show 2 + n = 1 + (n + 1) by cutsat) ▸ hf
obtain ⟨p₁, p₂, hp₁ | hp₂, h'⟩ := hg₂.eq_isMonicOfDegree_one_or_two_mul
· rw [h', ← mul_assoc] at h hf
exact ⟨g₁ * p₁, p₂, hd₁.mul hp₁, (hd₁.mul hp₁).of_mul_left hf, h⟩
· rw [h', mul_left_comm] at h hf
exact ⟨p₁, g₁ * p₂, hp₂, of_mul_left hp₂ hf, h⟩
· exact ⟨g₁, g₂, hd₂, of_mul_left hd₂ hf, h⟩
