fix(LinearAlgebra/{Free,Tensor,Clifford}Algebra): remove an unused `S…

…MulCommClass` argument (#8373) `SMulCommClass R S A` is always true when `Algebra R A` and `Algebra S A` and `A` is commutative, since the two actions factor via multiplication in `A`. I don't think mathlib actually knows this fact yet, but in this particular case it's also true by definition.
leanprover-community · Nov 12, 2023 · 30d39f9 · 30d39f9
1 parent 4cb02b4
commit 30d39f9
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 4 deletions.
diff --git a/Mathlib/Algebra/FreeAlgebra.lean b/Mathlib/Algebra/FreeAlgebra.lean
@@ -281,8 +281,7 @@ instance {R S A} [CommSemiring R] [CommSemiring S] [CommSemiring A]
     simp only [Algebra.algebraMap_eq_smul_one, smul_eq_mul]
     rw [smul_assoc, ←smul_one_mul]
 
-instance {R S A} [CommSemiring R] [CommSemiring S] [CommSemiring A]
-    [Algebra R A] [Algebra S A] [SMulCommClass R S A] :
+instance {R S A} [CommSemiring R] [CommSemiring S] [CommSemiring A] [Algebra R A] [Algebra S A] :
     SMulCommClass R S (FreeAlgebra A X) where
   smul_comm r s x := smul_comm (algebraMap R A r) (algebraMap S A s) x
 

diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
@@ -97,7 +97,7 @@ instance instAlgebra : Algebra R (CliffordAlgebra Q) := instAlgebra' _
 
 instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommGroup M] [CommRing A]
     [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M] (Q : QuadraticForm A M)
-    [IsScalarTower R A M] [IsScalarTower S A M] [SMulCommClass R S A] :
+    [IsScalarTower R A M] [IsScalarTower S A M] :
     SMulCommClass R S (CliffordAlgebra Q) :=
   RingQuot.instSMulCommClass _
 

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
@@ -81,7 +81,7 @@ example : (algebraNat : Algebra ℕ (TensorAlgebra R M)) = instAlgebra := rfl
 
 instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [CommSemiring A]
     [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M]
-    [IsScalarTower R A M] [IsScalarTower S A M] [SMulCommClass R S A] :
+    [IsScalarTower R A M] [IsScalarTower S A M] :
     SMulCommClass R S (TensorAlgebra A M) :=
   RingQuot.instSMulCommClass _