Commit 2022-04-12 03:21 bf1b813e

chore(algebra/module/basic): generalize to add_monoid_hom_class (#13346) I need some of these lemmas for ring_hom. Additionally, this:

• removes map_nat_module_smul (duplicate of map_nsmul) and map_int_module_smul (duplicate of map_zsmul)
• renames map_rat_module_smul to map_rat_smul for brevity.
• adds the lemmas inv_nat_cast_smul_comm and inv_int_cast_smul_comm.
• Swaps the order of the arguments to map_zsmul and map_nsmul to align with the usual rules (to_additive emitted them in the wrong order)