Commit 2021-03-17 19:18 7e82bba0

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.