annIdealGenerator_aeval_eq_zero — Mathlib

English

Evaluating the annihilating ideal generator at a yields zero: aeval a (annIdealGenerator 𝕜 a) = 0.

Русский

Пользуясь подстановкой по a, получаем ноль: aeval a (annIdealGenerator 𝕜 a) = 0.

LaTeX

$$$\operatorname{aeval}_a\big(\operatorname{annIdealGenerator}_{\mathbb{k}}(a)\big) = 0.$$$

Lean4

theorem annIdealGenerator_aeval_eq_zero (a : A) : aeval a (annIdealGenerator 𝕜 a) = 0 :=
  mem_annIdeal_iff_aeval_eq_zero.mp (annIdealGenerator_mem 𝕜 a)

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