mathlib3

0d3f8a71 - feat(ring_theory/submonoid/membership): generalize a few lemmas to `mul_mem_class` (#13748)

feat(ring_theory/submonoid/membership): generalize a few lemmas to `mul_mem_class` (#13748) This generalizes lemmas relating to the additive closure of a multiplicative monoid so that they also apply to multiplicative semigroups using `mul_mem_class`