Commit 2025-04-06 17:49 ad66b2ff

View on Github →

chore(RingTheory/Spectrum/Prime): fix statement of zeroLocus_eq_top_iff and golf (#23700)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

deleted theorem AlgebraicGeometry.Scheme.zeroLocus_eq_top_iff_subset_nilradical

deleted theorem AlgebraicGeometry.Scheme.zeroLocus_eq_top_iff_subset_nilradical_of_isCompact

added theorem AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical

added theorem AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact

Modified Mathlib/RingTheory/Spectrum/Prime/Basic.lean

added theorem PrimeSpectrum.vanishingIdeal_univ

deleted theorem PrimeSpectrum.zeroLocus_eq_top_iff

added theorem PrimeSpectrum.zeroLocus_eq_univ_iff

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean