Commit 2022-05-16 09:18 f0db51d4

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