mem_iff_annIdealGenerator_dvd — Mathlib

English

A polynomial p lies in the annihilating ideal 𝕜 a if and only if annIdealGenerator 𝕜 a divides p.

Русский

Полином p принадлежит аннигиляционному идеалу тогда и только тогда, когда annIdealGenerator 𝕜 a делит p.

LaTeX

$$$\forall p\in 𝕜[X],\ p \in \operatorname{annIdeal}_{\mathbb{k}}(a) \iff \operatorname{annIdealGenerator}_{\mathbb{k}}(a) \mid p.$$$

Lean4

theorem mem_iff_annIdealGenerator_dvd {p : 𝕜[X]} {a : A} : p ∈ annIdeal 𝕜 a ↔ annIdealGenerator 𝕜 a ∣ p := by
  rw [← Ideal.mem_span_singleton, span_singleton_annIdealGenerator]

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