Mathlib v3 is deprecated. Go to Mathlib v4

Def arrow_mul_distrib_mul_action

Modification history

2021-09-16 13:26
src/group_theory/group_action/group.lean
feat(group_theory/group_action): add `distrib_mul_action.to_add_aut` and `mul_distrib_mul_action.to_mul_aut` (#9224) …
Added arrow_mul_distrib_mul_actionView on Github →