Commit 2021-02-17 11:38 3c157512

feat(ring_theory/ideal/operations) : add lemma prod_eq_bot (#5795) Add lemma prod_eq_bot showing that a product of ideals in an integral domain is zero if and only if one of the terms is zero.