ker_aeval_eq_span_minpoly — Mathlib

English

For any A-algebra B and element x ∈ B, the kernel of the aeval map at x equals the A[X]-submodule generated by minpoly_A(x): ker(aeval x) = A[X] · minpoly_A x.

Русский

Для элемента x ∈ B верно: ядро отображения aeval_x равно порождающему подмодулю A[X] минполиномa_A(x).

LaTeX

$$RingHom.ker (Polynomial.aeval x) = A[X] ∙ minpoly A x$$

Lean4

/-- See also `minpoly.ker_eval` which relaxes the assumptions on `A` in exchange for
stronger assumptions on `B`. -/
@[simp]
theorem ker_aeval_eq_span_minpoly : RingHom.ker (Polynomial.aeval x) = A[X] ∙ minpoly A x :=
  by
  ext p
  simp_rw [RingHom.mem_ker, ← minpoly.dvd_iff, Submodule.mem_span_singleton, dvd_iff_exists_eq_mul_left, smul_eq_mul,
    eq_comm (a := p)]

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