exists_irreducible_of_degree_pos — Mathlib

English

If a polynomial f ∈ D[X] has positive degree, there exists an irreducible polynomial g such that g ∣ f.

Русский

Если полином f в D[X] имеет положительную степень, то существует ирреκбельный полином g, делающий g|f.

LaTeX

$$$$\\deg f > 0 \\Rightarrow \\exists g\\; \\big( \\text{Irreducible } g \\land g\\mid f \\big).$$$$

Lean4

theorem exists_irreducible_of_degree_pos (hf : 0 < f.degree) : ∃ g, Irreducible g ∧ g ∣ f :=
  WfDvdMonoid.exists_irreducible_factor (fun huf => ne_of_gt hf <| degree_eq_zero_of_isUnit huf) fun hf0 =>
    not_lt_of_gt hf <| hf0.symm ▸ (@degree_zero R _).symm ▸ WithBot.bot_lt_coe _

Похожие утверждения