Commit 2024-03-11 12:06 5176bb0d

View on Github →

feat(RingTheory/UniqueFactorizationDomain): add lemma UniqueFactorizationMonoid.IsPrime.exists_mem_Prime_of_neq_bot (#11218) We add UniqueFactorizationMonoid.IsPrime.exists_mem_Prime_of_neq_bot: if an integral domain is a UniqueFactorizationMonoid, then every nonzero prime ideal contains a prime element. We plan to add the other implication (known as Kaplansky's criterion) in a future PR.

Estimated changes

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.IsPrime.multiset_prod_mem_iff_exists_mem

added theorem Ideal.IsPrime.prod_mem_iff_exists_mem

Modified Mathlib/RingTheory/UniqueFactorizationDomain.lean

added theorem Ideal.IsPrime.exists_mem_prime_of_ne_bot