8.1. The left multiplication action🔗

As mentioned in Mathematics in Lean, the typeclass MulAction G X allows us to write g • x for the action of a group element g : G on an element x : X. Given types G and X, only one action can be inferred (since we need an unambiguous value for g • x). In the case where the literature has multiple actions, one of them is chosen as the default action. For instance, given G = X and [Group G] the action of G on itself by left multiplication is chosen as the default action.