annIdealGenerator_mem — Mathlib

English

The annihilating ideal generator annIdealGenerator 𝕜 a belongs to the annihilating ideal annIdeal 𝕜 a.

Русский

Генератор аннигиляторного идеала annIdealGenerator 𝕜 a принадлежит аннигиляторному идеалу annIdeal 𝕜 a.

LaTeX

$$$\operatorname{annIdealGenerator}_{\mathbb{k}}(a) \in \operatorname{annIdeal}_{\mathbb{k}}(a).$$$

Lean4

/-- The annihilating ideal generator is a member of the annihilating ideal. -/
theorem annIdealGenerator_mem (a : A) : annIdealGenerator 𝕜 a ∈ annIdeal 𝕜 a :=
  Ideal.mul_mem_right _ _ (Submodule.IsPrincipal.generator_mem _)

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