isIntegrallyClosed_dvd_iff — Mathlib

English

If s is integral over R and p monic with p(s)=0, then degree(minpoly(s)) ≤ degree(p).

Русский

Если s интегрален над R и p моноиком так, что p(s)=0, то deg(minpoly(s)) ≤ deg(p).

LaTeX

$$$\text{IsIntegral}(R,s) \Rightarrow p(s)=0 \Rightarrow \deg(\minpoly\ R\ s) \le \deg(p)$$$

Lean4

theorem isIntegrallyClosed_dvd_iff {s : S} (hs : IsIntegral R s) (p : R[X]) :
    Polynomial.aeval s p = 0 ↔ minpoly R s ∣ p :=
  ⟨fun hp => isIntegrallyClosed_dvd hs hp, fun hp => by
    simpa only [RingHom.mem_ker, RingHom.coe_comp, coe_evalRingHom, coe_mapRingHom, Function.comp_apply, eval_map,
      ← aeval_def] using aeval_eq_zero_of_dvd_aeval_eq_zero hp (minpoly.aeval R s)⟩

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