mem_annIdeal_iff_aeval_eq_zero — Mathlib

English

For every element a of a ring A equipped with an R-algebra structure and every polynomial p with coefficients in R, p belongs to the annihilating ideal annIdeal R a if and only if the evaluation of p at a is zero in A, i.e. aeval a p = 0.

Русский

Для любого элемента a кольца A с рациональной структурой над R и любого многочлена p с коэффициентами в R полином p принадлежит аннигилирующему идеалу annIdeal R a тогда и только тогда, когда подстановка a в p даёт ноль в A, то есть aeval a p = 0.

LaTeX

$$$\forall a\,\in A\,\forall p\,\in R[X],\; p\in \operatorname{annIdeal}_R(a) \iff \operatorname{aeval}_a(p)=0$$$

Lean4

/-- It is useful to refer to ideal membership sometimes
and the annihilation condition other times. -/
theorem mem_annIdeal_iff_aeval_eq_zero {a : A} {p : R[X]} : p ∈ annIdeal R a ↔ aeval a p = 0 :=
  Iff.rfl

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