Mathlib v3 is deprecated. Go to Mathlib v4

Def mul_semiring_action.to_alg_equiv

Modification history

2022-12-09 09:32
src/algebra/algebra/basic.lean
refactor(algebra/algebra): split alg_hom and alg_equiv to separate files (#17868) …
Modified mul_semiring_action.to_alg_equivView on Github →
2021-08-31 21:31
src/algebra/algebra/basic.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_alg_equivView on Github →