Commit 2021-03-01 10:35 aff6bd1b

fix(group_action/defs): make mul_action.regular an instance (#6241) This is essentially already an instance via semiring.to_semimodule.to_distrib_mul_action.to_mul_action, but with an unecessary semiring R constraint. I can't remember the details, but I've run into multiple instance resolution issues in the past that were resolved with local attribute [instance] mul_action.regular. This also renames the instance to monoid.to_mul_action for consistency with semiring.to_semimodule.