English
If f ∈ ℝ[X] is monic of degree ≥ 1, then f = f1 · f2 with f1 monic of degree 1 and f2 monic of degree deg(f) − 1.
Русский
Если f ∈ ℝ[X] монный степени ≥ 1, то f = f1 · f2, где deg f1 = 1 и deg f2 = deg f − 1, и f1, f2 мононичны.
LaTeX
$$$$\exists f_1,f_2:\mathbb{R}[X],\; f=f_1 f_2,\; \deg f_1=1,\; \deg f_2=\deg f-1.$$$$
Lean4
/-- 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 eq_isMonicOfDegree_one_mul_isMonicOfDegree {F : Type*} [Field F] [IsAlgClosed F] {f : F[X]} {n : ℕ}
(hf : IsMonicOfDegree f (n + 1)) : ∃ f₁ f₂ : F[X], IsMonicOfDegree f₁ 1 ∧ IsMonicOfDegree f₂ n ∧ f = f₁ * f₂ :=
by
obtain ⟨f₁, hf₁m, hf₁i, f₂, hf₂⟩ :=
exists_monic_irreducible_factor f <| not_isUnit_of_natDegree_pos f <| by grind [IsMonicOfDegree.natDegree_eq]
rw [hf₂, add_comm] at hf
have hf₁ : IsMonicOfDegree f₁ 1 :=
⟨natDegree_eq_of_degree_eq_some <| IsAlgClosed.degree_eq_one_of_irreducible F hf₁i, hf₁m⟩
exact ⟨f₁, f₂, hf₁, hf₁.of_mul_left hf, hf₂⟩
