Theorem Ideal.IsPrime.exists_mem_prime_of_ne_bot

Modification history

2026-01-20 16:34
Mathlib/RingTheory/UniqueFactorizationDomain/Ideal.lean
chore(Algebra): deprecate `CancelMonoidWithZero` (#33851) …
Modified Ideal.IsPrime.exists_mem_prime_of_ne_botView on Github →
2024-11-20 11:43
Mathlib/RingTheory/UniqueFactorizationDomain.lean
chore(RingTheory): split `UniqueFactorizationDomain.lean` (#19256) …
Modified Ideal.IsPrime.exists_mem_prime_of_ne_botView on Github →
2024-03-11 12:06
Mathlib/RingTheory/UniqueFactorizationDomain.lean
feat(RingTheory/UniqueFactorizationDomain): add lemma UniqueFactorizationMonoid.IsPrime.exists_mem_Prime_of_neq_bot (#11218) …
Added Ideal.IsPrime.exists_mem_prime_of_ne_botView on Github →