Theorem PrimeSpectrum.zeroLocus_eq_univ_iff

Modification history

2025-04-06 17:49

Mathlib/RingTheory/Spectrum/Prime/Basic.lean

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

Added PrimeSpectrum.zeroLocus_eq_univ_iff View on Github →