English
Same content as irreducible_iff_lt_natDegree_lt: an irreducible polynomial over a field has positive degree, and vice versa under the non-unit nonzero constraint.
Русский
То же самое, что и irreducible_iff_lt_natDegree_lt: неразложимый многочлен над полем имеет положительную степень, и обратно при условиях не единицы и не нуля.
LaTeX
$$$\text{Irreducible}(p) \iff ∀ q, \ Monic q \to natDegree q ∈ Finset.Ioc 0 (natDegree p / 2) \to ¬ q ∣ p$.$$
Lean4
/-- An irreducible polynomial over a field must have positive degree. -/
theorem natDegree_pos (h : Irreducible f) : 0 < f.natDegree :=
Nat.pos_of_ne_zero fun H ↦ by
obtain ⟨x, hf⟩ := natDegree_eq_zero.1 H
by_cases hx : x = 0
· rw [← hf, hx, map_zero] at h; exact not_irreducible_zero h
exact h.1 (hf ▸ isUnit_C.2 (Ne.isUnit hx))
