Revision #3360 → #3910 · back to history
a2f5c2f423d7| Field | From #3360 | To #3910 |
|---|---|---|
| mathlib.decl | Ideal.bot_prime | Ideal.isPrime_bot |
| note | `Ideal.bot_prime` shows the zero ideal `⊥ = {0}` is prime in any nontrivial domain, which ℤ is. | `Ideal.isPrime_bot` shows the zero ideal `⊥ = {0}` is prime in any nontrivial semiring with no zero divisors, which ℤ is. |