Commit 2022-05-02 11:44 61d5d308
View on Github →feat(group_theory/group_action/basic): A multiplicative action induces an additive action of the additive group (#13780)
mul_action M α induces add_action (additive M) α.
feat(group_theory/group_action/basic): A multiplicative action induces an additive action of the additive group (#13780)
mul_action M α induces add_action (additive M) α.