From 84ab233e305d7da1358a16013d19648d7322c506 Mon Sep 17 00:00:00 2001 From: FR Date: Thu, 10 Oct 2024 01:21:46 +0800 Subject: [PATCH] Update Defs.lean --- Mathlib/Algebra/GroupWithZero/Action/Defs.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/GroupWithZero/Action/Defs.lean b/Mathlib/Algebra/GroupWithZero/Action/Defs.lean index baf1b397954044..28a7f1306d857c 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*) [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.