Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-26 05:11
0a215a98
View on Github →
feat: port AlgebraicGeometry.PrimeSpectrum.Noetherian (
#4364
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/AlgebraicGeometry/PrimeSpectrum/Noetherian.lean
added
theorem
PrimeSpectrum.exists_primeSpectrum_prod_le
added
theorem
PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain