Mathlib Map

Theorems · Theorem · algebraic geometry

PrimeSpectrum.isClopen_iff

∀ {R : Type u} [inst : CommRing R] {s : Set (PrimeSpectrum R)},
  IsClopen s ↔ ∃ e, IsIdempotentElem e ∧ s = ↑(PrimeSpectrum.basicOpen e)
Defined in
Mathlib.RingTheory.Spectrum.Prime.Topology
Cited by
2 results in Mathlib
Foundations
Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

PrimeSpectrum.isClopen_iff_zeroLocus · cited by 1PrimeSpectrum.isClopen_if…Algebra.QuasiFiniteAt.of_isOpen_singleton · cited by 1QuasiFiniteAt.of_isOpen_s…Set · cited by 53352SetCommRing · cited by 17173CommRingSetLike.coe · cited by 8199SetLike.coeTopologicalSpace.Opens · cited by 2040TopologicalSpace.OpensIsClosed · cited by 1639IsClosedPrimeSpectrum · cited by 625PrimeSpectrumIsIdempotentElem · cited by 217IsIdempotentElemIsClopen · cited by 189IsClopenPrimeSpectrum.basicOpen · cited by 163PrimeSpectrum.basicOpenTopologicalSpace.Opens.is_open' · cited by 139Opens.is_open'PrimeSpectrum.isClosed_zeroLocus · cited by 10PrimeSpectrum.isClosed_ze…PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem · cited by 3PrimeSpectrum.basicOpen_e…PrimeSpectrum.exists_idempotent_basicOpen_eq_of_isClopen · cited by 2PrimeSpectrum.exists_idem…PrimeSpectrum.isClopen_iffCITED BYCITES

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.