Commit 2021-10-08 07:33 c4006779

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.