refactor(number_theory/modular_forms/slash_actions): slash actions are families of distrib_mul_actions

[eric-wieser]

This replaces the bespoke slash_action β G α γ typeclass with:

• Π b : β, distrib_mul_action (slash_act G b) α for the action itself, where slash_act G b is a type alias of mul_opposite (to allow for right actions)
• smul_comm_class (slash_act G k) γ α for compatibility with the γ action

This means compatibility with multiple types simultaneously is possible, and that f ∣[k;γ] A notation can be discarded.

This keeps around slash_action.map k A f to provide f ∣[k] A notation, but it's now reducibly equal to slash_act.of k A • f

---

It's not immediately clear that the switch to using distrib_mul_action is worth it, but this does at least prove it can be done.