basic): A multiplicative action induces an additive action of the additive group (#13780)

Commit

3 years ago

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) α`.

Author

tb65536

Parents

320df450

mathlib3 61d5d308 - feat(group_theory/group_action/basic): A multiplicative action induces an additive action of the additive group (#13780)

mathlib3
61d5d308 - feat(group_theory/group_action/basic): A multiplicative action induces an additive action of the additive group (#13780)