Mathlib v3 is deprecated. Go to Mathlib v4

Def distrib_mul_action.to_module_aut

Modification history

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