Commit 2024-12-20 16:26 fa580ede

View on Github →

feat: isomorphic rings have isomorphic spectra (#20068) ... and other simple lemmas about zeroLocus. From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib/RingTheory/PrimeSpectrum.lean

added def PrimeSpectrum.comapEquiv

added theorem PrimeSpectrum.zeroLocus_diff_singleton_zero

added theorem PrimeSpectrum.zeroLocus_insert_zero

added theorem PrimeSpectrum.zeroLocus_smul_of_isUnit