Theorem Ideal.IsPrime.prod_mem_iff_exists_mem

Modification history

2024-03-11 12:06
Mathlib/RingTheory/Ideal/Operations.lean
feat(RingTheory/UniqueFactorizationDomain): add lemma UniqueFactorizationMonoid.IsPrime.exists_mem_Prime_of_neq_bot (#11218) …
Added Ideal.IsPrime.prod_mem_iff_exists_memView on Github →