mathlib3

436966c1 - chore(data/finsupp/basic): generalize comap_mul_action (#11900)

chore(data/finsupp/basic): generalize comap_mul_action (#11900) This new definition is propoitionally equal to the old one in the presence of `[group G]` (all the previous `lemma`s continue to apply), but generalizes to `[monoid G]`. This also removes `finsupp.comap_distrib_mul_action_self` as there is no need to have this as a separate definition.