MulAction

structure MulAction[G: Group, X] {
    act: (G, X) -> X
} constraint {
    is_mul_action(act)
}

A left action of a group on a type.

GitHub

---

act

MulAction.act: (MulAction[G, X], G, X) -> X

The action map.