From 1247737e64e6480c9a8ad91a719b90db7266df29 Mon Sep 17 00:00:00 2001 From: FR Date: Wed, 9 Oct 2024 21:26:32 +0800 Subject: [PATCH] revert --- Mathlib/Algebra/GroupWithZero/Action/Defs.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Algebra/GroupWithZero/Action/Defs.lean b/Mathlib/Algebra/GroupWithZero/Action/Defs.lean index d241ec952f64e..baf1b39795404 100644 --- 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*) [Monoid M] [AddMonoid A] extends MulAction M A where +class DistribMulAction (M A : Type*) [outParam (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,7 +231,6 @@ section variable [Monoid M] [AddMonoid A] [DistribMulAction M A] -- See note [lower instance priority] -set_option synthInstance.checkSynthOrder false in instance (priority := 100) DistribMulAction.toDistribSMul {M A} {_ : Monoid M} {_ : AddMonoid A} [DistribMulAction M A] : DistribSMul M A := { ‹DistribMulAction M A› with }