Commit 2024-11-26 22:40 095a1c66

feat: semiring with discrete PrimeSpectrum (#19496) If the prime spectrum of a commutative semiring R has discrete Zariski topology, then R is canonically isomorphic to the product of its localizations at the (finitely many) maximal ideals. This was previously only proven for commutative rings R; a different proof using the sheaf property is required to generalize it.