Mathlib v3 is deprecated. Go to Mathlib v4

Def mul_semiring_action.to_semiring_equiv

Modification history

2021-08-31 21:31
src/algebra/group_ring_action.lean
feat(algebra/{module/linear_map, algebra/basic}): Add `distrib_mul_action.to_linear_(map|equiv)` and `mul_semiring_action.to_alg_(hom|equiv)` (#8936) …
Deleted mul_semiring_action.to_semiring_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 mul_semiring_action.to_semiring_equivView on Github →