mathlib4
mathlib4 copied to clipboard
feat(AlgebraicGeometry/PrimeSpectrum): prime spectrum of jacobson rings
PR summary 31393ef306
Import changes for modified files
No significant changes to the import graph
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.AlgebraicGeometry.PrimeSpectrum.Jacobson |
1384 |
Declarations diff
+ exists_isClosed_singleton_of_isJacobson
+ finite_setOf_isMin
+ isMax_iff
+ isMin_iff
+ isOpen_singleton_tfae_of_isNoetherian_of_isJacobson
+ stableUnderGeneralization_singleton
+ stableUnderSpecialization_singleton
+ zeroLocus_eq_iff
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>
The doc-module for script/declarations_diff.sh contains some details about this script.