Commit 2024-10-29 19:34 f5694384

View on Github →

feat(AlgebraicGeometry/PrimeSpectrum): description of clopen subsets in Spec R (#18394)

Estimated changes

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

added theorem PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem

added theorem PrimeSpectrum.exists_idempotent_basicOpen_eq_of_is_clopen

added theorem PrimeSpectrum.isClopen_iff

added theorem PrimeSpectrum.isClopen_iff_zeroLocus

added theorem PrimeSpectrum.isCompact_isOpen_iff

added theorem PrimeSpectrum.isCompact_isOpen_iff_ideal

added theorem PrimeSpectrum.zeroLocus_eq_basicOpen_of_isIdempotentElem