English
Over a field F, every non-unit polynomial f ∈ F[X] has a monic irreducible factor g with g ∣ f.
Русский
Над полем F каждый ненуль-под единицей полином f ∈ F[X] имеет моноичный ирред. делитель g, такой что g|f.
LaTeX
$$$$\\exists g\\in F[X],\\; g\\text{ monic} \\\\ g\\text{ irreducible} \\land g \\mid f.$$$$
Lean4
/-- A polynomial over a field which is not a unit must have a monic irreducible factor.
See also `WfDvdMonoid.exists_irreducible_factor`. -/
theorem 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⟩
