mathlib3

bf1b813e - chore(algebra/module/basic): generalize to add_monoid_hom_class (#13346)

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)