English
For f ∈ ℝ[X] monic with positive degree, there exists f1 and f2 with deg f1 ∈ {1,2} such that f = f1 · f2.
Русский
Для f ∈ ℝ[X] мононичного с положительной степенью существуют f1 и f2, такие что deg f1 ∈ {1,2} и f = f1 · f2.
LaTeX
$$$$\exists f_1,f_2:\mathbb{R}[X],\; (\deg f_1=1 \lor \deg f_1=2) \land f=f_1 f_2.$$$$
Lean4
/-- 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`. -/
-- TODO: generalize to real closed fields when they are available.
theorem eq_isMonicOfDegree_one_or_two_mul {f : ℝ[X]} {n : ℕ} (hf : IsMonicOfDegree f (n + 1)) :
∃ f₁ f₂ : ℝ[X], (IsMonicOfDegree f₁ 1 ∨ IsMonicOfDegree f₁ 2) ∧ f = f₁ * f₂ :=
by
obtain ⟨f₁, hm, hirr, f₂, hf₂⟩ :=
exists_monic_irreducible_factor f <| not_isUnit_of_natDegree_pos f <| by grind [IsMonicOfDegree.natDegree_eq]
refine ⟨f₁, f₂, ?_, hf₂⟩
have help {P : ℕ → Prop} {m : ℕ} (hm₀ : 0 < m) (hm₂ : m ≤ 2) (h : P m) : P 1 ∨ P 2 := by interval_cases m <;> tauto
exact help hirr.natDegree_pos hirr.natDegree_le_two <| IsMonicOfDegree.mk rfl hm
