[Merged by Bors] - fix(group_action/defs): make mul_action.regular an instance

[eric-wieser]

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.

---

[jcommelin]

The reason this wasn't an instance, is that there are other natural actions that one might want to make into an instance locally, such as the conjugation action. Apparently your patch doesn't break mathlib, which surprises me a bit 😉
But I'm still not sure if this is a good idea. @ChrisHughes24 @kckennylau what do you think?

[eric-wieser]

I agree, but I figured those arguments apply to semiring.to_semimodule too, and it seems that we ended up with that as an instance.

[jcommelin]

No, I don't think those arguments apply to the semiring situation. I'm not aware of other ways to turn a ring into a module over itself that are common in maths. But groups acting on themselves in various ways are quite common.

[eric-wieser]

I'm not aware of other ways to turn a ring into a module over itself that are common in maths.

Sorry - my point was about ways to turn a ring into a mul_action over itself (not a semimodule), and semiring.to_semimodule provides that transitively. If R is a field, then both the "multiply" and "conjugation" actions would be a valid instance.

[Vierkantor]

I started a discussion on Zulip to get this PR going again: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.236241.20make.20mul_action.2Eregular.20an.20instance

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests