English
A minimal polynomial is irreducible over A when x is integral over A.
Русский
Минимальный полином ирредуцируем над A, если x интегрирован над A.
LaTeX
$$$\text{Irreducible}(\minpoly A x)$$$
Lean4
/-- A minimal polynomial is irreducible. -/
theorem irreducible (hx : IsIntegral A x) : Irreducible (minpoly A x) :=
by
refine (irreducible_of_monic (monic hx) <| ne_one A x).2 fun f g hf hg he => ?_
rw [← hf.isUnit_iff, ← hg.isUnit_iff]
by_contra! h
have heval := congr_arg (Polynomial.aeval x) he
rw [aeval A x, aeval_mul, mul_eq_zero] at heval
rcases heval with heval | heval
· exact aeval_ne_zero_of_dvdNotUnit_minpoly hx hf ⟨hf.ne_zero, g, h.2, he.symm⟩ heval
· refine aeval_ne_zero_of_dvdNotUnit_minpoly hx hg ⟨hg.ne_zero, f, h.1, ?_⟩ heval
rw [mul_comm, he]
