vanishingIdeal_eq_top_iff — Mathlib

English

zeroLocus of a set equals univ iff that set is contained in nilradical.

Русский

нулевой локус множества равен всему если множество содержится в нилрадикале.

LaTeX

$$$ \operatorname{zeroLocus}(s) = \mathrm{Set.univ} \iff s \subseteq \operatorname{nilradical}(R) $$$

Lean4

theorem vanishingIdeal_eq_top_iff {s : Set (PrimeSpectrum R)} : vanishingIdeal s = ⊤ ↔ s = ∅ := by
  rw [← top_le_iff, ← subset_zeroLocus_iff_le_vanishingIdeal, Submodule.top_coe, zeroLocus_univ, Set.subset_empty_iff]

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