Mathlib v3 is deprecated. Go to Mathlib v4

Def mul_distrib_mul_action.to_mul_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 mul_distrib_mul_action.to_mul_equivView on Github →
2021-09-08 14:00
src/algebra/group_ring_action.lean
feat(group_theory/group_action): Extract a smaller typeclass out of `mul_semiring_action` (#8918) …
Added mul_distrib_mul_action.to_mul_equivView on Github →