ker_eval — Mathlib

English

In integrally closed settings, the evaluation map’s kernel equals the span of the minimal polynomial.

Русский

В интегрально закрытых условиях ядро отображения совпадает с породнителем минимального полинома.

LaTeX

$$$\ker(\mathrm{aeval}_s) = (minpoly_R(s))$$$

Lean4

theorem ker_eval {s : S} (hs : IsIntegral R s) :
    RingHom.ker ((Polynomial.aeval s).toRingHom : R[X] →+* S) = Ideal.span ({minpoly R s} : Set R[X]) :=
  by
  ext p
  simp_rw [RingHom.mem_ker, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, isIntegrallyClosed_dvd_iff hs, ←
    Ideal.mem_span_singleton]

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