perf: use implicit parameters in SMul hierarchy

leanprover-community · Oct 9, 2024 · ac90eed · ac90eed
1 parent 5ddd0ae
commit ac90eed
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 4 deletions.
diff --git a/Mathlib/Algebra/Algebra/Defs.lean b/Mathlib/Algebra/Algebra/Defs.lean
@@ -237,7 +237,8 @@ theorem algebra_ext {R : Type*} [CommSemiring R] {A : Type*} [Semiring A] (P Q :
   congr
 
 -- see Note [lower instance priority]
-instance (priority := 200) toModule : Module R A where
+instance (priority := 200) toModule {R A} {_ : CommSemiring R} {_ : Semiring A} [Algebra R A] :
+    Module R A where
   one_smul _ := by simp [smul_def']
   mul_smul := by simp [smul_def', mul_assoc]
   smul_add := by simp [smul_def', mul_add]

diff --git a/Mathlib/Algebra/Module/Defs.lean b/Mathlib/Algebra/Module/Defs.lean
@@ -67,7 +67,8 @@ variable [Semiring R] [AddCommMonoid M] [Module R M] (r s : R) (x y : M)
 
 -- see Note [lower instance priority]
 /-- A module over a semiring automatically inherits a `MulActionWithZero` structure. -/
-instance (priority := 100) Module.toMulActionWithZero : MulActionWithZero R M :=
+instance (priority := 100) Module.toMulActionWithZero
+  {R M} {_ : Semiring R} {_ : AddCommMonoid M} [Module R M] : MulActionWithZero R M :=
   { (inferInstance : MulAction R M) with
     smul_zero := smul_zero
     zero_smul := Module.zero_smul }

diff --git a/Mathlib/Algebra/Ring/Action/Basic.lean b/Mathlib/Algebra/Ring/Action/Basic.lean
@@ -46,7 +46,8 @@ variable (M N G : Type*) [Monoid M] [Monoid N] [Group G]
 variable (A R S F : Type v) [AddMonoid A] [Semiring R] [CommSemiring S]
 
 -- note we could not use `extends` since these typeclasses are made with `old_structure_cmd`
-instance (priority := 100) MulSemiringAction.toMulDistribMulAction [h : MulSemiringAction M R] :
+instance (priority := 100) MulSemiringAction.toMulDistribMulAction
+    (M R) {_ : Monoid M} {_ : Semiring R} [h : MulSemiringAction M R] :
     MulDistribMulAction M R :=
   { h with }
 

diff --git a/Mathlib/Algebra/SMulWithZero.lean b/Mathlib/Algebra/SMulWithZero.lean
@@ -126,7 +126,8 @@ class MulActionWithZero extends MulAction R M where
   zero_smul : ∀ m : M, (0 : R) • m = 0
 
 -- see Note [lower instance priority]
-instance (priority := 100) MulActionWithZero.toSMulWithZero [m : MulActionWithZero R M] :
+instance (priority := 100) MulActionWithZero.toSMulWithZero
+    (R M) {_ : MonoidWithZero R} {_ : Zero M} [m : MulActionWithZero R M] :
     SMulWithZero R M :=
   { m with }