Mathlib v3 is deprecated. Go to Mathlib v4

Def mul_semiring_action.to_ring_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) …
Added mul_semiring_action.to_ring_equivView on Github →