nits

Co-authored-by: Eric Wieser <[email protected]>
leanprover-community · Dec 7, 2024 · 3139716 · 3139716
1 parent 3187e7f
commit 3139716
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/RingTheory/AdicCompletion/Basic.lean b/Mathlib/RingTheory/AdicCompletion/Basic.lean
@@ -245,12 +245,12 @@ instance [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] :
   Subtype.val_injective.module S f val_smul
 
 instance instIsScalarTower [SMul T S] [SMul T R] [SMul S R] [SMul T M] [SMul S M]
-    [IsScalarTower S R M] [IsScalarTower T S M] [IsScalarTower T R M] :
+    [IsScalarTower S R M] [IsScalarTower T R M] [IsScalarTower T S M] :
     IsScalarTower T S (AdicCompletion I M) where
   smul_assoc r s f := by ext; simp [val_smul]
 
 instance instSMulCommClass [SMul T R] [SMul S R] [SMul T M] [SMul S M]
-    [IsScalarTower S R M] [SMulCommClass T S M] [IsScalarTower T R M] :
+    [IsScalarTower S R M] [IsScalarTower T R M] [SMulCommClass T S M] :
     SMulCommClass T S (AdicCompletion I M) where
   smul_comm r s f := by ext; simp [val_smul, smul_comm]