mem_iff_eq_smul_annIdealGenerator

English

Every polynomial p ∈ annIdeal 𝕜 a can be written as a multiple of annIdealGenerator 𝕜 a: p = s · annIdealGenerator 𝕜 a for some s ∈ 𝕜[X].

Русский

Любой полином p ∈ annIdeal 𝕜 a можно записать как произведение на annIdealGenerator 𝕜 a: p = s · annIdealGenerator 𝕜 a для некоторого s ∈ 𝕜[X].

LaTeX

$$$\forall p\in \mathbb{k}[X],\ p\in \operatorname{annIdeal}_{\mathbb{k}}(a) \iff \exists s\in \mathbb{k}[X],\ p = s\cdot \operatorname{annIdealGenerator}_{\mathbb{k}}(a).$$$

Lean4

theorem mem_iff_eq_smul_annIdealGenerator {p : 𝕜[X]} (a : A) :
    p ∈ annIdeal 𝕜 a ↔ ∃ s : 𝕜[X], p = s • annIdealGenerator 𝕜 a := by
  simp_rw [@eq_comm _ p, ← mem_span_singleton, ← span_singleton_annIdealGenerator 𝕜 a, Ideal.span]

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