Revision #1485 → #2153 · back to history
modifiedZero ring has no prime idealsbf5a6c30f242
| Field | From #1485 | To #2153 |
|---|
| mathlib.decl | PrimeSpectrum.instIsEmpty | PrimeSpectrum.isEmpty_iff_subsingleton |
| mathlib.match_kind | related | exact |
| note | The prime spectrum of the zero ring is empty (`IsEmpty (PrimeSpectrum R)` for a `Subsingleton` ring): any prime needs `I ≠ ⊤`, but `⊤ = ⊥` there. | `PrimeSpectrum.isEmpty_iff_subsingleton : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R` (with a Subsingleton instance giving `IsEmpty (PrimeSpectrum R)`) exactly says the zero ring has no prime ideals. |
modifiedPositive powers of a non-nilpotent element form a prototypical m-system4c01777a15a5
| Field | From #1485 | To #2153 |
|---|
| mathlib.match_kind | related | special_case |
modifiedCommutative ring in which every proper ideal is prime is a field4285df8c8e33
| Field | From #1485 | To #2153 |
|---|
| mathlib.match_kind | related | special_case |
modifiedPositive powers of a non-nilpotent element form a prototypical m-systemc1b2c6a73d19
| Field | From #1485 | To #2153 |
|---|
| mathlib.match_kind | related | special_case |