Mathlib Changelog
v4
Changelog
About
Github
Theorem
Ideal.IsPrime.multiset_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.multiset_prod_mem_iff_exists_mem
View on Github →