ker_evalRingHom — Mathlib

English

For a monic q, the kernel of modByMonicHom q is the scalar restriction of the principal ideal (q).

Русский

Для моноичного q ядро модуля modByMonicHom q равно распространению по скалярам идеала (q).

LaTeX

$$$\operatorname{LinearMap}.ker(q.\text{modByMonicHom}) = (\operatorname{Ideal}.span\{q\}).restrictScalars R$$$

Lean4

theorem ker_evalRingHom (x : R) : RingHom.ker (evalRingHom x) = Ideal.span {X - C x} :=
  by
  ext y
  simp [Ideal.mem_span_singleton, dvd_iff_isRoot, RingHom.mem_ker]

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