…#11972)

Previously `module R' (continuous_multilinear_map A M₁ M₂)` required `algebra R' A`, but now it only requires `smul_comm_class A R' M₂`.

The old instance required (modulo argument reordering):
```lean
def continuous_multilinear_map.module {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι]
  [Π i, add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π i, topological_space (M₁ i)]
  [topological_space M₂] [has_continuous_add M₂] 
  {R' : Type u_1} {A : Type u_2} [comm_semiring R'] [semiring A] [topological_space R']
  [Π i, module A (M₁ i)]  [module A M₂] [module R' M₂] [has_continuous_smul R' M₂]
  [algebra R' A] [is_scalar_tower R' A M₂] :
    module R' (continuous_multilinear_map A M₁ M₂)
```
while the new one requires
```lean
def continuous_multilinear_map.module {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι]
  [Π i, add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π i, topological_space (M₁ i)]
  [topological_space M₂] [has_continuous_add M₂]
  {R' : Type u_1} {A : Type u_2} [semiring R'] [semiring A] [topological_space R']  -- note: `R'` not commutative any more
  [Π i, module A (M₁ i)] [module A M₂] [module R' M₂] [has_continuous_smul R' M₂]
  [smul_comm_class A R' M₂] :  -- note: `R'` needs no action at all on `A`
    module R' (continuous_multilinear_map A M₁ M₂)
```

This change also adds intermediate `mul_action` and `distrib_mul_action` instances which apply in weaker situations.

As a result of this weakening, the typeclass arguments to `continuous_multilinear_map.to_normed_space` can also be weakened, and a weird instance workaround can be removed.