Commit 2024-01-08 13:15 3b800125

View on Github →

feat : generalize PrimeSpectrum from Ring to Semiring (#8763) Some results of PrimeSpectrum generalized from CommRing to CommSemiring.

Estimated changes

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

modified theorem LocalRing.PrimeSpectrum.comap_residue

modified theorem LocalRing.comap_closedPoint

modified theorem LocalRing.isLocalRingHom_iff_comap_closedPoint

modified def PrimeSpectrum.closedsEmbedding

modified theorem PrimeSpectrum.localization_away_comap_range

modified theorem PrimeSpectrum.localization_away_openEmbedding

modified structure PrimeSpectrum