diff --git a/Mathlib.lean b/Mathlib.lean
index 37a1220f1968e1..aa3af524b5f540 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2213,6 +2213,7 @@ import Mathlib.LinearAlgebra.BilinearForm.TensorProduct
 import Mathlib.LinearAlgebra.BilinearMap
 import Mathlib.LinearAlgebra.Charpoly.Basic
 import Mathlib.LinearAlgebra.Charpoly.ToMatrix
+import Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
 import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
 import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
 import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
new file mode 100644
index 00000000000000..ee26f754e4e311
--- /dev/null
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
@@ -0,0 +1,201 @@
+/-
+Copyright (c) 2023 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import Mathlib.Data.Complex.Module
+import Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
+import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
+import Mathlib.LinearAlgebra.TensorProduct.Opposite
+import Mathlib.RingTheory.TensorProduct
+
+/-!
+# The base change of a clifford algebra
+
+In this file we show the isomorphism
+
+* `CliffordAlgebra.equivBaseChange A Q` :
+  `CliffordAlgebra (Q.baseChange A) ≃ₐ[A] (A ⊗[R] CliffordAlgebra Q)`
+  with forward direction `CliffordAlgebra.toBasechange A Q` and reverse direction
+  `CliffordAlgebra.ofBasechange A Q`.
+
+This covers a more general case of the complexification of clifford algebras (as described in §2.2
+of https://empg.maths.ed.ac.uk/Activities/Spin/Lecture2.pdf), where ℂ and ℝ are replaced by an
+`R`-algebra `A` (where `2 : R` is invertible).
+
+We show the additional results:
+
+* `CliffordAlgebra.toBasechange_ι`: the effect of base-changing pure vectors.
+* `CliffordAlgebra.ofBasechange_tmul_ι`: the effect of un-base-changing a tensor of a pure vectors.
+* `CliffordAlgebra.toBasechange_involute`: the effect of base-changing an involution.
+* `CliffordAlgebra.toBasechange_reverse`: the effect of base-changing a reversal.
+-/
+
+variable {R A V : Type*}
+variable [CommRing R] [CommRing A] [AddCommGroup V]
+variable [Algebra R A] [Module R V] [Module A V] [IsScalarTower R A V]
+variable [Invertible (2 : R)]
+
+open scoped TensorProduct
+
+namespace CliffordAlgebra
+
+variable (A)
+
+/-- Auxiliary construction: note this is really just a heterobasic `CliffordAlgebra.map`. -/
+def ofBaseChangeAux (Q : QuadraticForm R V) :
+    CliffordAlgebra Q →ₐ[R] CliffordAlgebra (Q.baseChange A) :=
+  CliffordAlgebra.lift Q <| by
+    refine ⟨(ι (Q.baseChange A)).restrictScalars R ∘ₗ TensorProduct.mk R A V 1, fun v => ?_⟩
+    refine (CliffordAlgebra.ι_sq_scalar (Q.baseChange A) (1 ⊗ₜ v)).trans ?_
+    rw [QuadraticForm.baseChange_tmul, one_mul, ←Algebra.algebraMap_eq_smul_one,
+      ←IsScalarTower.algebraMap_apply]
+
+@[simp] theorem ofBaseChangeAux_ι (Q : QuadraticForm R V) (v : V) :
+    ofBaseChangeAux A Q (ι Q v) = ι (Q.baseChange A) (1 ⊗ₜ v) :=
+  CliffordAlgebra.lift_ι_apply _ _ v
+
+/-- Convert from the base-changed clifford algebra to the clifford algebra over a base-changed
+module. -/
+def ofBaseChange (Q : QuadraticForm R V) :
+    A ⊗[R] CliffordAlgebra Q →ₐ[A] CliffordAlgebra (Q.baseChange A) :=
+  Algebra.TensorProduct.algHomOfLinearMapTensorProduct
+    (TensorProduct.AlgebraTensorModule.lift <|
+      let f : A →ₗ[A] _ := (Algebra.lsmul A A (CliffordAlgebra (Q.baseChange A))).toLinearMap
+      LinearMap.flip <| LinearMap.flip (({
+        toFun := fun f : CliffordAlgebra (Q.baseChange A) →ₗ[A] CliffordAlgebra (Q.baseChange A) =>
+          LinearMap.restrictScalars R f
+        map_add' := fun f g => LinearMap.ext fun x => rfl
+        map_smul' := fun (c : A) g => LinearMap.ext fun x => rfl
+      } : _ →ₗ[A] _) ∘ₗ f) ∘ₗ (ofBaseChangeAux A Q).toLinearMap)
+    (fun z₁ z₂ b₁ b₂ =>
+      show (z₁ * z₂) • ofBaseChangeAux A Q (b₁ * b₂)
+        = z₁ • ofBaseChangeAux A Q b₁ * z₂ • ofBaseChangeAux A Q b₂
+      by rw [map_mul, smul_mul_smul])
+    (fun r =>
+      show r • ofBaseChangeAux A Q 1 = algebraMap A (CliffordAlgebra (Q.baseChange A)) r
+      by rw [map_one, Algebra.algebraMap_eq_smul_one])
+
+@[simp] theorem ofBaseChange_tmul_ι (Q : QuadraticForm R V) (z : A) (v : V) :
+    ofBaseChange A Q (z ⊗ₜ ι Q v) = ι (Q.baseChange A) (z ⊗ₜ v) := by
+  show z • ofBaseChangeAux A Q (ι Q v) = ι (Q.baseChange A) (z ⊗ₜ[R] v)
+  rw [ofBaseChangeAux_ι, ←map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
+
+@[simp] theorem ofBaseChange_tmul_one (Q : QuadraticForm R V) (z : A) :
+    ofBaseChange A Q (z ⊗ₜ 1) = algebraMap _ _ z := by
+  show z • ofBaseChangeAux A Q 1 = _
+  rw [map_one, ←Algebra.algebraMap_eq_smul_one]
+
+/-- Convert from the clifford algebra over a base-changed module to the base-changed clifford
+algebra. -/
+def toBaseChange (Q : QuadraticForm R V) :
+    CliffordAlgebra (Q.baseChange A) →ₐ[A] A ⊗[R] CliffordAlgebra Q :=
+  CliffordAlgebra.lift _ <| by
+    refine ⟨TensorProduct.AlgebraTensorModule.map (LinearMap.id : A →ₗ[A] A) (ι Q), ?_⟩
+    letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
+    letI : Invertible (2 : A ⊗[R] CliffordAlgebra Q) :=
+      (Invertible.map (algebraMap R _) 2).copy 2 (map_ofNat _ _).symm
+    suffices hpure_tensor : ∀ v w, (1 * 1) ⊗ₜ[R] (ι Q v * ι Q w) + (1 * 1) ⊗ₜ[R] (ι Q w * ι Q v) =
+        QuadraticForm.polarBilin (Q.baseChange A) (1 ⊗ₜ[R] v) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1 by
+      -- the crux is that by converting to a statement about linear maps instead of quadratic forms,
+      -- we then have access to all the partially-applied `ext` lemmas.
+      rw [CliffordAlgebra.forall_mul_self_eq_iff (isUnit_of_invertible _)]
+      refine TensorProduct.AlgebraTensorModule.curry_injective ?_
+      ext v w
+      exact hpure_tensor v w
+    intros v w
+    rw [← TensorProduct.tmul_add, CliffordAlgebra.ι_mul_ι_add_swap,
+      QuadraticForm.polarBilin_baseChange, BilinForm.baseChange_tmul, one_mul,
+      TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one, QuadraticForm.polarBilin_apply]
+
+@[simp] theorem toBaseChange_ι (Q : QuadraticForm R V) (z : A) (v : V) :
+    toBaseChange A Q (ι (Q.baseChange A) (z ⊗ₜ v)) = z ⊗ₜ ι Q v :=
+  CliffordAlgebra.lift_ι_apply _ _ _
+
+theorem toBaseChange_comp_involute (Q : QuadraticForm R V) :
+    (toBaseChange A Q).comp (involute : CliffordAlgebra (Q.baseChange A) →ₐ[A] _) =
+      (Algebra.TensorProduct.map (AlgHom.id _ _) involute).comp (toBaseChange A Q) := by
+  ext v
+  show toBaseChange A Q (involute (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))
+    = (Algebra.TensorProduct.map (AlgHom.id _ _) involute :
+        A ⊗[R] CliffordAlgebra Q →ₐ[A] _)
+      (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))
+  rw [toBaseChange_ι, involute_ι, map_neg (toBaseChange A Q), toBaseChange_ι,
+    Algebra.TensorProduct.map_tmul, AlgHom.id_apply, involute_ι, TensorProduct.tmul_neg]
+
+/-- The involution acts only on the right of the tensor product. -/
+theorem toBaseChange_involute (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.baseChange A)) :
+    toBaseChange A Q (involute x) =
+      TensorProduct.map LinearMap.id (involute.toLinearMap) (toBaseChange A Q x) :=
+  FunLike.congr_fun (toBaseChange_comp_involute A Q) x
+
+open MulOpposite
+
+/-- Auxiliary theorem used to prove `toBaseChange_reverse` without needing induction. -/
+theorem toBaseChange_comp_reverseOp (Q : QuadraticForm R V) :
+    (toBaseChange A Q).op.comp (reverseOp) =
+      ((Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)).toAlgHom.comp <|
+        (Algebra.TensorProduct.map
+          (AlgEquiv.toOpposite A A).toAlgHom (reverseOp (Q := Q))).comp
+        (toBaseChange A Q)) := by
+  ext v
+  show op (toBaseChange A Q (reverse (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) =
+    Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)
+      (Algebra.TensorProduct.map (AlgEquiv.toOpposite A A).toAlgHom (reverseOp (Q := Q))
+        (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v))))
+  rw [toBaseChange_ι, reverse_ι, toBaseChange_ι, Algebra.TensorProduct.map_tmul,
+    Algebra.TensorProduct.opAlgEquiv_tmul, reverseOp_ι]
+  rfl
+
+/-- `reverse` acts only on the right of the tensor product. -/
+theorem toBaseChange_reverse (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.baseChange A)) :
+    toBaseChange A Q (reverse x) =
+      TensorProduct.map LinearMap.id reverse (toBaseChange A Q x) := by
+  have := FunLike.congr_fun (toBaseChange_comp_reverseOp A Q) x
+  refine (congr_arg unop this).trans ?_; clear this
+  refine (LinearMap.congr_fun (TensorProduct.AlgebraTensorModule.map_comp _ _ _ _).symm _).trans ?_
+  rw [reverse, ←AlgEquiv.toLinearMap, ←AlgEquiv.toLinearEquiv_toLinearMap,
+    AlgEquiv.toLinearEquiv_toOpposite]
+  simp
+  rfl
+
+attribute [ext] TensorProduct.ext
+
+theorem toBaseChange_comp_ofBaseChange (Q : QuadraticForm R V) :
+    (toBaseChange A Q).comp (ofBaseChange A Q) = AlgHom.id _ _ := by
+  ext z : 2
+  · change toBaseChange A Q (ofBaseChange A Q (z ⊗ₜ[R] 1)) = z ⊗ₜ[R] 1
+    rw [ofBaseChange_tmul_one, AlgHom.commutes, Algebra.TensorProduct.algebraMap_apply,
+      Algebra.id.map_eq_self]
+  · ext v : 1
+    change toBaseChange A Q (ofBaseChange A Q (1 ⊗ₜ[R] ι Q v)) = 1 ⊗ₜ[R] ι Q v
+    rw [ofBaseChange_tmul_ι, toBaseChange_ι]
+
+@[simp] theorem toBaseChange_ofBaseChange (Q : QuadraticForm R V) (x : A ⊗[R] CliffordAlgebra Q) :
+    toBaseChange A Q (ofBaseChange A Q x) = x :=
+  AlgHom.congr_fun (toBaseChange_comp_ofBaseChange A Q : _) x
+
+theorem ofBaseChange_comp_toBaseChange (Q : QuadraticForm R V) :
+    (ofBaseChange A Q).comp (toBaseChange A Q) = AlgHom.id _ _ := by
+  ext x
+  show ofBaseChange A Q (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] x)))
+    = ι (Q.baseChange A) (1 ⊗ₜ[R] x)
+  rw [toBaseChange_ι, ofBaseChange_tmul_ι]
+
+@[simp] theorem ofBaseChange_toBaseChange
+    (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.baseChange A)) :
+    ofBaseChange A Q (toBaseChange A Q x) = x :=
+  AlgHom.congr_fun (ofBaseChange_comp_toBaseChange A Q : _) x
+
+/-- Base-changing the vector space of a clifford algebra is isomorphic as an A-algebra to
+base-changing the clifford algebra itself; <|Cℓ(A ⊗_R V, Q_A) ≅ A ⊗_R Cℓ(V, Q)<|.
+
+This is `CliffordAlgebra.toBaseChange` and `CliffordAlgebra.ofBaseChange` as an equivalence. -/
+@[simps!]
+def equivBaseChange (Q : QuadraticForm R V) :
+    CliffordAlgebra (Q.baseChange A) ≃ₐ[A] A ⊗[R] CliffordAlgebra Q :=
+  AlgEquiv.ofAlgHom (toBaseChange A Q) (ofBaseChange A Q)
+    (toBaseChange_comp_ofBaseChange A Q)
+    (ofBaseChange_comp_toBaseChange A Q)
+
+end CliffordAlgebra
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
index b4736e34f0409f..9b9eea02676ef0 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
@@ -230,16 +230,36 @@ theorem induction {C : CliffordAlgebra Q → Prop}
   exact Subtype.prop (lift Q of a)
 #align clifford_algebra.induction CliffordAlgebra.induction
 
-/-- The symmetric product of vectors is a scalar -/
-theorem ι_mul_ι_add_swap (a b : M) :
-    ι Q a * ι Q b + ι Q b * ι Q a = algebraMap R _ (QuadraticForm.polar Q a b) :=
+theorem mul_add_swap_eq_polar_of_forall_mul_self_eq {A : Type*} [Ring A] [Algebra R A]
+    (f : M →ₗ[R] A) (hf : ∀ x, f x * f x = algebraMap _ _ (Q x)) (a b : M) :
+    f a * f b + f b * f a = algebraMap R _ (QuadraticForm.polar Q a b) :=
   calc
-    ι Q a * ι Q b + ι Q b * ι Q a = ι Q (a + b) * ι Q (a + b) - ι Q a * ι Q a - ι Q b * ι Q b := by
-      rw [(ι Q).map_add, mul_add, add_mul, add_mul]; abel
+    f a * f b + f b * f a = f (a + b) * f (a + b) - f a * f a - f b * f b := by
+      rw [f.map_add, mul_add, add_mul, add_mul]; abel
     _ = algebraMap R _ (Q (a + b)) - algebraMap R _ (Q a) - algebraMap R _ (Q b) := by
-      rw [ι_sq_scalar, ι_sq_scalar, ι_sq_scalar]
+      rw [hf, hf, hf]
     _ = algebraMap R _ (Q (a + b) - Q a - Q b) := by rw [← RingHom.map_sub, ← RingHom.map_sub]
     _ = algebraMap R _ (QuadraticForm.polar Q a b) := rfl
+
+/-- An alternative way to provide the argument to `CliffordAlgebra.lift` when `2` is invertible.
+
+To show a function squares to the quadratic form, it suffices to show that
+`f x * f y + f y * f x = algebraMap _ _ (polar Q x y)` -/
+theorem forall_mul_self_eq_iff {A : Type*} [Ring A] [Algebra R A] (h2 : IsUnit (2 : A))
+    (f : M →ₗ[R] A) :
+    (∀ x, f x * f x = algebraMap _ _ (Q x)) ↔
+      (LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f =
+        Q.polarBilin.toLin.compr₂ (Algebra.linearMap R A) := by
+  simp_rw [FunLike.ext_iff]
+  refine ⟨mul_add_swap_eq_polar_of_forall_mul_self_eq _, fun h x => ?_⟩
+  change ∀ x y : M, f x * f y + f y * f x = algebraMap R A (QuadraticForm.polar Q x y) at h
+  apply h2.mul_left_cancel
+  rw [two_mul, two_mul, h x x, QuadraticForm.polar_self, two_mul, map_add]
+
+/-- The symmetric product of vectors is a scalar -/
+theorem ι_mul_ι_add_swap (a b : M) :
+    ι Q a * ι Q b + ι Q b * ι Q a = algebraMap R _ (QuadraticForm.polar Q a b) :=
+  mul_add_swap_eq_polar_of_forall_mul_self_eq _ (ι_sq_scalar _) _ _
 #align clifford_algebra.ι_mul_ι_add_swap CliffordAlgebra.ι_mul_ι_add_swap
 
 theorem ι_mul_comm (a b : M) :