remove unused argument. The linter did not find it :(

leanprover-community · Jul 23, 2023 · 5bd526b · 5bd526b
1 parent 23a1289
commit 5bd526b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Algebra/RingQuot.lean b/Mathlib/Algebra/RingQuot.lean
@@ -273,7 +273,7 @@ instance [CommSemiring T] [SMul S T] [Algebra S R] [Algebra T R] [IsScalarTower
     IsScalarTower S T (RingQuot r) :=
   ⟨fun s t ⟨a⟩ => Quot.inductionOn a <| fun a' => by simp only [RingQuot.smul_quot, smul_assoc]⟩
 
-instance [CommSemiring T] [SMul S T] [Algebra S R] [Algebra T R] [SMulCommClass S T R] :
+instance [CommSemiring T] [Algebra S R] [Algebra T R] [SMulCommClass S T R] :
     SMulCommClass S T (RingQuot r) :=
   ⟨fun s t ⟨a⟩ => Quot.inductionOn a <| fun a' => by simp only [RingQuot.smul_quot, smul_comm]⟩