Commit 2021-11-14 15:22 5307dc1b

feat(data/equiv/module): add module.to_module_End (#10300) The new definitions are:

• distrib_mul_action.to_module_End
• distrib_mul_action.to_module_aut
• module.to_module_End Everything else is a move. This also moves the group structure on linear_equiv earlier in the import heirarchy. This is more consistent with where it is for linear_map.