mathlib

e289343a - feat(algebra/graded_monoid): add lemmas about power and product membership (#10627)

feat(algebra/graded_monoid): add lemmas about power and product membership (#10627) This adds: * `set_like.graded_monoid.pow_mem` * `set_like.graded_monoid.list_prod_map_mem` * `set_like.graded_monoid.list_prod_of_fn_mem` It doesn't bother to add the multiset and finset versions for now, because these are not imported at this point, and require the ring to be commutative.