Commit 2022-02-07 17:28 436966c1

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 lemmas 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.