mathlib3

71e90063 - chore(topology/algebra/module/multilinear): relax typeclass arguments (#11972)

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): ```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.