English
For monic p, Irreducible p iff p ≠ 1 and for all monic f,g with f g = p, not both f.natDegree and g.natDegree are positive (i.e., one is 0).
Русский
Для моноического p: Irreducible p тогда и только тогда, когда p ≠ 1 и для любых моноичных f,g с f g = p не оба их natDegree положительны (один равен 0).
LaTeX
$$$Monic(p) \land p \neq 1 \Rightarrow Irreducible(p) \iff \forall f,g, fMonic \land gMonic \land f g = p \Rightarrow (natDegree(f) = 0 \lor natDegree(g) = 0)$$$
Lean4
theorem irreducible_iff_natDegree' (hp : p.Monic) :
Irreducible p ↔ p ≠ 1 ∧ ∀ f g : R[X], f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2) :=
by
simp_rw [hp.irreducible_iff_natDegree, mem_Ioc, Nat.le_div_iff_mul_le zero_lt_two, mul_two]
apply and_congr_right'
constructor <;> intro h f g hf hg he <;> subst he
· rw [hf.natDegree_mul hg, add_le_add_iff_right]
exact fun ha => (h f g hf hg rfl).elim (ha.1.trans_le ha.2).ne' ha.1.ne'
· simp_rw [hf.natDegree_mul hg, pos_iff_ne_zero] at h
contrapose! h
obtain hl | hl := le_total f.natDegree g.natDegree
· exact ⟨g, f, hg, hf, mul_comm g f, h.1, add_le_add_left hl _⟩
· exact ⟨f, g, hf, hg, rfl, h.2, add_le_add_right hl _⟩
