Mathlib v3 is deprecated. Go to Mathlib v4

Def distrib_mul_action.to_module_End

Modification history

2021-11-14 15:22
src/algebra/module/linear_map.lean
feat(data/equiv/module): add module.to_module_End (#10300) …
Added distrib_mul_action.to_module_EndView on Github →