From 3cf735536794d9bf544ce2c66694ab4988dc1939 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 2 Aug 2023 10:41:17 +0000
Subject: [PATCH] feat(LinearAlgebra/CliffordAlgebra): support towers of
 algebras (#6074)

---
 .../LinearAlgebra/CliffordAlgebra/Basic.lean  | 26 ++++++++++++++++++-
 1 file changed, 25 insertions(+), 1 deletion(-)

diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
index a7f18be72dcc3..760b6668c5c94 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
+++ b/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 :=