English
For a polynomial p over a field, if p ≠ 0 and p is not a unit, then p is irreducible if and only if every divisor q of p with deg(q) ≤ deg(p)/2 is a unit.
Русский
Для многочлена p над полем, если p ≠ 0 и не является единицей, то p неразложим тогда и только тогда, когда каждый делитель q,m степень которого удовлетворяет deg(q) ≤ deg(p)/2, является единицей.
LaTeX
$$$p \neq 0,\; \lnot \text{IsUnit}(p) \Longrightarrow\ \text{Irreducible}(p) \iff \forall q,\ q.deg \le \frac{\operatorname{natDegree}(p)}{2} \to q \mid p \to \text{IsUnit}(q).$$$
Lean4
/-- To check a polynomial over a field is irreducible, it suffices to check only for
divisors that have smaller degree.
See also: `Polynomial.Monic.irreducible_iff_natDegree`.
-/
theorem irreducible_iff_degree_lt (p : R[X]) (hp0 : p ≠ 0) (hpu : ¬IsUnit p) :
Irreducible p ↔ ∀ q, q.degree ≤ ↑(natDegree p / 2) → q ∣ p → IsUnit q :=
by
rw [← irreducible_mul_leadingCoeff_inv, (monic_mul_leadingCoeff_inv hp0).irreducible_iff_degree_lt]
· simp [hp0, natDegree_mul_leadingCoeff_inv]
· contrapose! hpu
exact isUnit_of_mul_eq_one _ _ hpu
