English
For monic p and p ≠ 1, p is irreducible iff for all monic f,g with f g = p, either f = 1 or g = 1.
Русский
Для моноического p и p ≠ 1 полином ирредуцируем тогда и только тогда, когда для любых моноических f,g с f g = p верно: либо f = 1 либо g = 1.
LaTeX
$$$Monic(p) \land p \neq 1 \Rightarrow (Irreducible\,p \iff \forall f,g, fMonic \land gMonic \land f g = p \Rightarrow (f=1 \lor g=1))$$$
Lean4
theorem irreducible_of_monic (hp : p.Monic) (hp1 : p ≠ 1) :
Irreducible p ↔ ∀ f g : R[X], f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1 :=
by
refine
⟨fun h f g hf hg hp => (h.2 hp.symm).imp hf.eq_one_of_isUnit hg.eq_one_of_isUnit, fun h =>
⟨hp1 ∘ hp.eq_one_of_isUnit, fun f g hfg =>
(h (g * C f.leadingCoeff) (f * C g.leadingCoeff) ?_ ?_ ?_).symm.imp (isUnit_of_mul_eq_one f _)
(isUnit_of_mul_eq_one g _)⟩⟩
· rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, mul_comm, ← hfg, ← Monic]
· rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, ← hfg, ← Monic]
· rw [mul_mul_mul_comm, ← C_mul, ← leadingCoeff_mul, ← hfg, hp.leadingCoeff, C_1, mul_one, mul_comm, ← hfg]
