mathlib3

79fbd465 - feat(ring_theory/ideal): generalize two results from finset to multiset (#8320)

feat(ring_theory/ideal): generalize two results from finset to multiset (#8320) Nothing exciting going on here, just copied two proofs, replaced all `finset.insert` with `multiset.cons` and `finset.prod` with `(multiset.map _).prod`, and used those to show the original results.