mathlib

4e8d9666 - feat(algebra/subalgebra): add missing actions by and on subalgebras (#9081)

feat(algebra/subalgebra): add missing actions by and on subalgebras (#9081) For `S : subalgebra R A`, this adds the instances: * for actions on subalgebras (generalizing the existing `algebra R S`): * `module R' S` * `algebra R' S` * `is_scalar_tower R' R S` * for actions by subalgebras (generalizing the existing `algebra S α`): * `mul_action S α` * `smul_comm_class S α β` * `smul_comm_class α S β` * `is_scalar_tower S α β` * `has_faithful_scalar S α` * `distrib_mul_action S α` * `module S α` This also removes the commutativity requirement on `A` for the `no_zero_smul_divisors S A` instance.