Commit 2022-02-12 08:07 71e90063

chore(topology/algebra/module/multilinear): relax typeclass arguments (#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):

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

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.