Mathlib v3 is deprecated. Go to Mathlib v4

Def distrib_mul_action.to_add_equiv

Modification history

2021-09-16 13:26
src/algebra/group_ring_action.lean
feat(group_theory/group_action): add `distrib_mul_action.to_add_aut` and `mul_distrib_mul_action.to_mul_aut` (#9224) …
Modified distrib_mul_action.to_add_equivView on Github →
2020-05-01 07:42
src/algebra/group_ring_action.lean
feat(algebra/group_ring_action) define group actions on rings (#2566) …
Added distrib_mul_action.to_add_equivView on Github →