Update Defs.lean

leanprover-community · Oct 9, 2024 · 84ab233 · 84ab233
1 parent 3e46ee9
commit 84ab233
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/Mathlib/Algebra/GroupWithZero/Action/Defs.lean b/Mathlib/Algebra/GroupWithZero/Action/Defs.lean
@@ -220,7 +220,7 @@ end DistribSMul
 
 /-- Typeclass for multiplicative actions on additive structures. This generalizes group modules. -/
 @[ext]
-class DistribMulAction (M A : Type*) [outParam (Monoid M)] [AddMonoid A] extends MulAction M A where
+class DistribMulAction (M A : Type*) [Monoid M] [AddMonoid A] extends MulAction M A where
   /-- Multiplying `0` by a scalar gives `0` -/
   smul_zero : ∀ a : M, a • (0 : A) = 0
   /-- Scalar multiplication distributes across addition -/
@@ -231,8 +231,7 @@ section
 variable [Monoid M] [AddMonoid A] [DistribMulAction M A]
 
 -- See note [lower instance priority]
-instance (priority := 100) DistribMulAction.toDistribSMul
-  {M A} {_ : Monoid M} {_ : AddMonoid A} [DistribMulAction M A] : DistribSMul M A :=
+instance (priority := 100) DistribMulAction.toDistribSMul : DistribSMul M A :=
   { ‹DistribMulAction M A› with }
 
 -- Porting note: this probably is no longer relevant.