English
For a monic p ∈ R[x], p is irreducible iff for all q with deg q ≤ deg(p)/2, q | p implies q is a unit.
Русский
Для моничного p ∈ R[x], p неприводим тогда и только тогда, когда для каждого q со степенью ≤ deg(p)/2, если q делит p, то q — единица.
LaTeX
$$p.Monic → p ≠ 0 → Irreducible p ↔ ∀ q, deg q ≤ deg(p)/2 → q | p → IsUnit q$$
Lean4
/-- To check a monic polynomial 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]} (p_monic : Monic p) (p_1 : p ≠ 1) :
Irreducible p ↔ ∀ q, degree q ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q :=
by
simp only [p_monic.irreducible_iff_lt_natDegree_lt p_1, Finset.mem_Ioc, and_imp, natDegree_pos_iff_degree_pos,
natDegree_le_iff_degree_le]
constructor
· rintro h q deg_le dvd
by_contra q_unit
have := degree_pos_of_not_isUnit_of_dvd_monic p_monic q_unit dvd
have hu := p_monic.isUnit_leadingCoeff_of_dvd dvd
refine (h _ (monic_of_isUnit_leadingCoeff_inv_smul hu) ?_ ?_ (dvd_trans ?_ dvd)).elim
· rwa [degree_smul_of_smul_regular _ (isSMulRegular_of_group _)]
· rwa [degree_smul_of_smul_regular _ (isSMulRegular_of_group _)]
· rw [Units.smul_def, Polynomial.smul_eq_C_mul, (isUnit_C.mpr (Units.isUnit _)).mul_left_dvd]
· rintro h q _ deg_pos deg_le dvd
exact deg_pos.ne' <| degree_eq_zero_of_isUnit (h q deg_le dvd)
