Commit 2021-09-08 10:25 4e8d9666

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.