zeroLocus_eq_singleton — Mathlib

English

For any x in PrimeSpectrum(R), IsMin x iff x.asIdeal ∈ minimalPrimes R.

Русский

Для любого x в PrimeSpectrum(R) IsMin x тогда и только тогда, когда x.asIdeal ∈ minimalPrimes R.

LaTeX

$$$IsMin\\ x \\iff x.asIdeal \\in minimalPrimes(R).$$$

Lean4

theorem zeroLocus_eq_singleton (m : Ideal R) [m.IsMaximal] : zeroLocus m = {⟨m, inferInstance⟩} :=
  by
  ext I
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · simp only [mem_zeroLocus, SetLike.coe_subset_coe] at h
    simpa using PrimeSpectrum.ext_iff.mpr (Ideal.IsMaximal.eq_of_le ‹_› I.2.ne_top h).symm
  · simp [Set.mem_singleton_iff.mp h]

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