chore: move generic SMul definition before AddMonoid or AddGroup instances to make sure they can use it (leanprover-community#40706)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/Algebra/Quaternion.lean

@@ -723,11 +723,14 @@ variable {S T R : Type*} [CommRing R] (r x y : R) (a b : ℍ[R])
 
 instance : CoeTC R ℍ[R] := ⟨coe⟩
 
-instance instRing : Ring ℍ[R] := inferInstanceAs <| Ring ℍ[R,-1,0,-1]
+instance [SMul S R] : SMul S ℍ[R] := inferInstanceAs <| SMul S ℍ[R,-1,0,-1]
 
-instance : Inhabited ℍ[R] := inferInstanceAs <| Inhabited ℍ[R,-1,0,-1]
+instance instRing : Ring ℍ[R] where
+  nsmul := letI := Quaternion.instSMul (S := ℕ) (R := R); (· • ·)
+  zsmul := letI := Quaternion.instSMul (S := ℤ) (R := R); (· • ·)
+  __ : Ring ℍ[R] := inferInstanceAs <| Ring ℍ[R,-1,0,-1]
 
-instance [SMul S R] : SMul S ℍ[R] := inferInstanceAs <| SMul S ℍ[R,-1,0,-1]
+instance : Inhabited ℍ[R] := inferInstanceAs <| Inhabited ℍ[R,-1,0,-1]
 
 instance [SMul S T] [SMul S R] [SMul T R] [IsScalarTower S T R] : IsScalarTower S T ℍ[R] :=
   inferInstanceAs <| IsScalarTower S T ℍ[R,-1,0,-1]

Mathlib/Algebra/TrivSqZeroExt/Basic.lean

@@ -197,11 +197,16 @@ instance addSemigroup [AddSemigroup R] [AddSemigroup M] : AddSemigroup (tsze R M
 instance addZeroClass [AddZeroClass R] [AddZeroClass M] : AddZeroClass (tsze R M) :=
   inferInstanceAs <| AddZeroClass (R × M)
 
-instance addMonoid [AddMonoid R] [AddMonoid M] : AddMonoid (tsze R M) :=
-  inferInstanceAs <| AddMonoid (R × M)
+instance smul [SMul S R] [SMul S M] : SMul S (tsze R M) :=
+  inferInstanceAs <| SMul S (R × M)
+
+instance addMonoid [AddMonoid R] [AddMonoid M] : AddMonoid (tsze R M) where
+  nsmul := letI := smul (S := ℕ) (R := R) (M := M); (· • ·)
+  __ : AddMonoid (tsze R M) := inferInstanceAs <| AddMonoid (R × M)
 
-instance addGroup [AddGroup R] [AddGroup M] : AddGroup (tsze R M) :=
-  inferInstanceAs <| AddGroup (R × M)
+instance addGroup [AddGroup R] [AddGroup M] : AddGroup (tsze R M) where
+  zsmul := letI := smul (S := ℤ) (R := R) (M := M); (· • ·)
+  __ : AddGroup (tsze R M) := inferInstanceAs <| AddGroup (R × M)
 
 instance addCommSemigroup [AddCommSemigroup R] [AddCommSemigroup M] : AddCommSemigroup (tsze R M) :=
   inferInstanceAs <| AddCommSemigroup (R × M)
@@ -212,9 +217,6 @@ instance addCommMonoid [AddCommMonoid R] [AddCommMonoid M] : AddCommMonoid (tsze
 instance addCommGroup [AddCommGroup R] [AddCommGroup M] : AddCommGroup (tsze R M) :=
   inferInstanceAs <| AddCommGroup (R × M)
 
-instance smul [SMul S R] [SMul S M] : SMul S (tsze R M) :=
-  inferInstanceAs <| SMul S (R × M)
-
 instance isScalarTower [SMul T R] [SMul T M] [SMul S R] [SMul S M] [SMul T S]
     [IsScalarTower T S R] [IsScalarTower T S M] : IsScalarTower T S (tsze R M) :=
   inferInstanceAs <| IsScalarTower T S (R × M)

Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean

@@ -141,8 +141,12 @@ instance instZero [Zero A] : Zero (CStarMatrix m n A) :=
 instance instAddZeroClass [AddZeroClass A] : AddZeroClass (CStarMatrix m n A) :=
   inferInstanceAs <| AddZeroClass (Matrix m n A)
 
-instance instAddMonoid [AddMonoid A] : AddMonoid (CStarMatrix m n A) :=
-  inferInstanceAs <| AddMonoid (Matrix m n A)
+instance instSMul [SMul R A] : SMul R (CStarMatrix m n A) :=
+  inferInstanceAs <| SMul R (Matrix m n A)
+
+instance instAddMonoid [AddMonoid A] : AddMonoid (CStarMatrix m n A) where
+  nsmul := letI := instSMul (R := ℕ) (A := A) (m := m) (n := n); (· • · )
+  __ : AddMonoid (CStarMatrix m n A) := inferInstanceAs <| AddMonoid (Matrix m n A)
 
 instance instAddCommMonoid [AddCommMonoid A] : AddCommMonoid (CStarMatrix m n A) :=
   inferInstanceAs <| AddCommMonoid (Matrix m n A)
@@ -153,8 +157,9 @@ instance instNeg [Neg A] : Neg (CStarMatrix m n A) :=
 instance instSub [Sub A] : Sub (CStarMatrix m n A) :=
   inferInstanceAs <| Sub (Matrix m n A)
 
-instance instAddGroup [AddGroup A] : AddGroup (CStarMatrix m n A) :=
-  inferInstanceAs <| AddGroup (Matrix m n A)
+instance instAddGroup [AddGroup A] : AddGroup (CStarMatrix m n A) where
+  zsmul := letI := instSMul (R := ℤ) (A := A) (m := m) (n := n); (· • · )
+  __ : AddGroup (CStarMatrix m n A) := inferInstanceAs <| AddGroup (Matrix m n A)
 
 instance instAddCommGroup [AddCommGroup A] : AddCommGroup (CStarMatrix m n A) :=
   inferInstanceAs <| AddCommGroup (Matrix m n A)
@@ -168,9 +173,6 @@ instance instSubsingleton [Subsingleton A] : Subsingleton (CStarMatrix m n A) :=
 instance instNontrivial [Nonempty m] [Nonempty n] [Nontrivial A] : Nontrivial (CStarMatrix m n A) :=
   inferInstanceAs <| Nontrivial (Matrix m n A)
 
-instance instSMul [SMul R A] : SMul R (CStarMatrix m n A) :=
-  inferInstanceAs <| SMul R (Matrix m n A)
-
 instance instSMulCommClass [SMul R A] [SMul S A] [SMulCommClass R S A] :
     SMulCommClass R S (CStarMatrix m n A) :=
   inferInstanceAs <| SMulCommClass R S (Matrix m n A)

Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

@@ -129,11 +129,16 @@ def AlgebraicClosure : Type u :=
 
 namespace AlgebraicClosure
 
-deriving instance CommRing, Inhabited for AlgebraicClosure
+deriving instance Inhabited for AlgebraicClosure
 
 instance {S : Type*} [DistribSMul S k] [IsScalarTower S k k] : SMul S (AlgebraicClosure k) :=
   inferInstanceAs <| SMul S (_ ⧸ _)
 
+instance : CommRing (AlgebraicClosure k) where
+  nsmul := letI := AlgebraicClosure.instSMulOfIsScalarTower k (S := ℕ); (· • · )
+  zsmul := letI := AlgebraicClosure.instSMulOfIsScalarTower k (S := ℤ); (· • · )
+  __ : CommRing (AlgebraicClosure k) := inferInstanceAs <| CommRing (_ ⧸ _)
+
 instance instAlgebra {R : Type*} [CommSemiring R] [Algebra R k] : Algebra R (AlgebraicClosure k) :=
   inferInstanceAs <| Algebra R (_ ⧸ _)
 

Mathlib/RingTheory/AdjoinRoot.lean

@@ -68,7 +68,18 @@ section CommRing
 
 variable [CommRing R] (f g : R[X])
 
-deriving instance CommRing, Inhabited for AdjoinRoot
+deriving instance Inhabited for AdjoinRoot
+
+instance instSMulAdjoinRoot [DistribSMul S R] [IsScalarTower S R R] : SMul S (AdjoinRoot f) :=
+  inferInstanceAs <| SMul S (_ ⧸ _)
+
+instance : CommRing (AdjoinRoot f) where
+  nsmul := letI := instSMulAdjoinRoot (S := ℕ) (R := R); (· • ·)
+  zsmul := letI := instSMulAdjoinRoot (S := ℤ) (R := R); (· • ·)
+  __ : CommRing (AdjoinRoot f) := inferInstanceAs <| CommRing (_ ⧸ _)
+
+instance [DistribSMul S R] [IsScalarTower S R R] : DistribSMul S (AdjoinRoot f) :=
+  inferInstanceAs <| DistribSMul S (_ ⧸ _)
 
 instance : DecidableEq (AdjoinRoot f) :=
   Classical.decEq _
@@ -92,12 +103,6 @@ theorem induction_on {C : AdjoinRoot f → Prop} (x : AdjoinRoot f) (ih : ∀ p
 def of : R →+* AdjoinRoot f :=
   (mk f).comp C
 
-instance instSMulAdjoinRoot [DistribSMul S R] [IsScalarTower S R R] : SMul S (AdjoinRoot f) :=
-  inferInstanceAs <| SMul S (_ ⧸ _)
-
-instance [DistribSMul S R] [IsScalarTower S R R] : DistribSMul S (AdjoinRoot f) :=
-  inferInstanceAs <| DistribSMul S (_ ⧸ _)
-
 @[simp]
 theorem smul_mk [DistribSMul S R] [IsScalarTower S R R] (a : S) (x : R[X]) :
     a • mk f x = mk f (a • x) :=