mathlib3
5307dc1b - feat(data/equiv/module): add module.to_module_End (#10300)

Commit
4 years ago
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`.
Author
Parents
Loading