mathlib3

c4006779 - feat(algebra/module/basic): `module rat E` is a subsingleton (#9570)

feat(algebra/module/basic): `module rat E` is a subsingleton (#9570) * allow different (semi)rings in `add_monoid_hom.map_int_cast_smul` and `add_monoid_hom.map_nat_cast_smul`; * add `add_monoid_hom.map_inv_int_cast_smul` and `add_monoid_hom.map_inv_nat_cast_smul`; * allow different division rings in `add_monoid_hom.map_rat_cast_smul`, drop `char_zero` assumption; * prove `subsingleton (module rat M)`; * add a few convenience lemmas. Co-authored-by: Johan Commelin <johan@commelin.net>