irreducible — Mathlib

English

If f is primitive and Eisenstein at a prime ideal P, and deg f > 0, then f is irreducible.

Русский

Если fPrimitive и Эйзенштейнов относительно простого идеала P, при этом deg f > 0, то f ирредуцируем.

LaTeX

$$$f.IsEisensteinAt 𝓟 \\to 𝓟.IsPrime \\to f.IsPrimitive \\to 0 < f.natDegree \\to Irreducible f$$$

Lean4

/-- If a primitive `f` satisfies `f.IsEisensteinAt 𝓟`, where `𝓟.IsPrime`,
then `f` is irreducible. -/
theorem irreducible (hf : f.IsEisensteinAt 𝓟) (hprime : 𝓟.IsPrime) (hu : f.IsPrimitive) (hfd0 : 0 < f.natDegree) :
    Irreducible f :=
  irreducible_of_eisenstein_criterion hprime hf.leading (fun _ hn => hf.mem (coe_lt_degree.1 hn))
    (natDegree_pos_iff_degree_pos.1 hfd0) hf.notMem hu

Похожие утверждения