English
For monic p of natDegree 2, not irreducible iff there exist c1,c2 with p.coeff 0 = c1 c2 and p.coeff 1 = c1 + c2.
Русский
Для моноичного p с natDegree = 2 неразложимость эквивалентна существованию c1,c2 таких, что p.coeff 0 = c1 c2 и p.coeff 1 = c1 + c2.
LaTeX
$$$Monic(p) \land p.natDegree = 2 \Rightarrow (Not Irreducible(p) \iff \exists c_1 \exists c_2, p.coeff 0 = c_1 c_2 \land p.coeff 1 = c_1 + c_2)$$$
Lean4
/-- Alternate phrasing of `Polynomial.Monic.irreducible_iff_natDegree'` where we only have to check
one divisor at a time. -/
theorem irreducible_iff_lt_natDegree_lt {p : R[X]} (hp : p.Monic) (hp1 : p ≠ 1) :
Irreducible p ↔ ∀ q, Monic q → natDegree q ∈ Finset.Ioc 0 (natDegree p / 2) → ¬q ∣ p :=
by
rw [hp.irreducible_iff_natDegree', and_iff_right hp1]
constructor
· rintro h g hg hdg ⟨f, rfl⟩
exact h f g (hg.of_mul_monic_left hp) hg (mul_comm f g) hdg
· rintro h f g - hg rfl hdg
exact h g hg hdg (dvd_mul_left g f)
