exists_irreducible_of_natDegree_pos

English

If natDegree f > 0 then there exists an irreducible g with g ∣ f.

Русский

Если natDegree f > 0, существует ирред. g с g|f.

LaTeX

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

Lean4

theorem exists_irreducible_of_natDegree_pos (hf : 0 < f.natDegree) : ∃ g, Irreducible g ∧ g ∣ f :=
  exists_irreducible_of_degree_pos <| by
    contrapose! hf
    exact natDegree_le_of_degree_le hf

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