Mathlib v3 is deprecated. Go to Mathlib v4

Def mul_distrib_mul_action.to_mul_aut

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 mul_distrib_mul_action.to_mul_autView on Github →