mathlib3

f0db51d4 - feat(algebra/module): morphism classes for (semi)linear maps (#13939)

feat(algebra/module): morphism classes for (semi)linear maps (#13939) This PR introduces morphism classes corresponding to `mul_action_hom`, `distrib_mul_action_hom`, `mul_semiring_action_hom` and `linear_map`. Most of the new generic results work smoothly, only `simp` seems to have trouble applying `map_smulₛₗ`. I expect this requires another fix in the elaborator along the lines of [lean#659](https://github.com/leanprover-community/lean/pull/659). For now we can just keep around the specialized `simp` lemmas `linear_map.map_smulₛₗ` and `linear_equiv.map_smulₛₗ`. The other changes are either making `map_smul` protected where it conflicts, or helping the elaborator unfold some definitions that previously were helped by the specific `map_smul` lemma suggesting the type. Thanks to @dupuisf for updating and making this branch compile! Co-Authored-By: Frédéric Dupuis <dupuisf@iro.umontreal.ca> Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca> Co-authored-by: Anne Baanen <t.baanen@vu.nl>