Commit 2022-04-28 17:35 0d3f8a71
View on Github →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