mathlib3

7e82bba0 - feat(algebra/module/submodule): add `smul_of_tower_mem` (#6712)

feat(algebra/module/submodule): add `smul_of_tower_mem` (#6712) This adds the lemmas: * `sub_mul_action.smul_of_tower_mem` * `submodule.smul_of_tower_mem` And uses them to construct the new scalar actions: * `sub_mul_action.mul_action'` * `sub_mul_action.is_scalar_tower` * `submodule.semimodule'` * `submodule.is_scalar_tower` With associated lemmas * `sub_mul_action.coe_smul_of_tower` * `submodule.coe_smul_of_tower` The unprimed instance continue to hold their old values, and exist to speed up typeclass search; the same pattern we use for `tensor_product.semimodule` vs `tensor_product.semimodule`. Co-authored-by: Vierkantor <vierkantor@vierkantor.com>