mathlib3

3c157512 - feat(ring_theory/ideal/operations) : add lemma prod_eq_bot (#5795)

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. Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Filippo A. E. Nuccio <65080144+faenuccio@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com>