feat(LinearAlgebra/CliffordAlgebra): support towers of algebras (#6074)

Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

@@ -79,9 +79,33 @@ instance instInhabited : Inhabited (CliffordAlgebra Q) := RingQuot.instInhabited
 #align clifford_algebra.inhabited CliffordAlgebra.instInhabited
 instance instRing : Ring (CliffordAlgebra Q) := RingQuot.instRing _
 #align clifford_algebra.ring CliffordAlgebra.instRing
-instance instAlgebra: Algebra R (CliffordAlgebra Q) := RingQuot.instAlgebraRingQuotInstSemiring _
+
+instance (priority := 900) instAlgebra' {R A M} [CommSemiring R] [AddCommGroup M] [CommRing A]
+    [Algebra R A] [Module R M] [Module A M] (Q : QuadraticForm A M)
+    [IsScalarTower R A M] :
+    Algebra R (CliffordAlgebra Q) :=
+  RingQuot.instAlgebraRingQuotInstSemiring _
+
+-- verify there are no diamonds
+example : (algebraNat : Algebra ℕ (CliffordAlgebra Q)) = instAlgebra' _ := rfl
+example : (algebraInt _ : Algebra ℤ (CliffordAlgebra Q)) = instAlgebra' _ := rfl
+
+-- shortcut instance, as the other instance is slow
+instance instAlgebra : Algebra R (CliffordAlgebra Q) := instAlgebra' _
 #align clifford_algebra.algebra CliffordAlgebra.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] :
+    SMulCommClass R S (CliffordAlgebra Q) :=
+  RingQuot.instSMulCommClassRingQuotInstSMulRingQuotInstSMulRingQuot _
+
+instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommGroup M] [CommRing A]
+    [SMul R S] [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M]
+    [IsScalarTower R A M] [IsScalarTower S A M] [IsScalarTower R S A] (Q : QuadraticForm A M) :
+    IsScalarTower R S (CliffordAlgebra Q) :=
+  RingQuot.instIsScalarTowerRingQuotInstSMulRingQuotInstSMulRingQuot _
+
 /-- The canonical linear map `M →ₗ[R] CliffordAlgebra Q`.
 -/
 def ι : M →ₗ[R] CliffordAlgebra Q :=