English
To check irreducibility over a field, it suffices to check there are no divisors q of p with 0 < deg(q) ≤ deg(p)/2; equivalently, if such q exist, p is not irreducible.
Русский
Чтобы проверить неразложимость над полем, достаточно проверить, что не существует делителя q с 0 < deg(q) ≤ deg(p)/2; эквивалентно: если такой q существует, p неразложим.
LaTeX
$$$\text{Irreducible}(p) \iff \forall q,\ Monic(q) \to natDegree(q) \in \mathrm{Finset.Ioc}(0, natDegree(p)/2) \to \neg q \mid p.$$$
Lean4
/-- To check a polynomial `p` over a field is irreducible, it suffices to check there are no
divisors of degree `0 < d ≤ degree p / 2`.
See also: `Polynomial.Monic.irreducible_iff_natDegree'`.
-/
theorem irreducible_iff_lt_natDegree_lt {p : R[X]} (hp0 : p ≠ 0) (hpu : ¬IsUnit p) :
Irreducible p ↔ ∀ q, Monic q → natDegree q ∈ Finset.Ioc 0 (natDegree p / 2) → ¬q ∣ p :=
by
have : p * C (leadingCoeff p)⁻¹ ≠ 1 := by
contrapose! hpu
exact isUnit_of_mul_eq_one _ _ hpu
rw [← irreducible_mul_leadingCoeff_inv, (monic_mul_leadingCoeff_inv hp0).irreducible_iff_lt_natDegree_lt this,
natDegree_mul_leadingCoeff_inv _ hp0]
simp only [IsUnit.dvd_mul_right
(isUnit_C.mpr (IsUnit.mk0 (leadingCoeff p)⁻¹ (inv_ne_zero (leadingCoeff_ne_zero.mpr hp0))))]
