isMaximal_iff_eq_vanishingIdeal_singleton

English

An ideal I is maximal iff there exists x with I = vanishingIdeal k {x}.

Русский

Идеал I максимален тогда и только тогда, когда существует x такой, что I = vanishingIdeal k {x}.

LaTeX

$$I.IsMaximal ↔ ∃ x : σ → K, I = vanishingIdeal k { x }$$

Lean4

theorem isMaximal_iff_eq_vanishingIdeal_singleton {I : Ideal (MvPolynomial σ K)} :
    I.IsMaximal ↔ ∃ x : σ → K, I = vanishingIdeal K { x } :=
  ⟨eq_vanishingIdeal_singleton_of_isMaximal K, fun ⟨_, hx⟩ => hx ▸ inferInstance⟩

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