English
For monic p, Irreducible p iff p ≠ 1 and for all monic f,g with f g = p, either natDegree f = 0 or natDegree g = 0.
Русский
Для моноического p: Irreducible p тогда и только тогда, когда p ≠ 1 и для любых моноичных f,g с f g = p либо natDegree f = 0, либо natDegree g = 0.
LaTeX
$$$Monic(p) \Rightarrow (Irreducible(p) \iff p \neq 1 \,\land\, \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 → f.natDegree = 0 ∨ g.natDegree = 0 :=
by
by_cases hp1 : p = 1; · simp [hp1]
rw [irreducible_of_monic hp hp1, and_iff_right hp1]
refine forall₄_congr fun a b ha hb => ?_
rw [ha.natDegree_eq_zero_iff_eq_one, hb.natDegree_eq_zero_iff_eq_one]
