diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean
index fc5bcda77af79..a183bc45667c2 100644
--- a/Mathlib/Algebra/Quaternion.lean
+++ b/Mathlib/Algebra/Quaternion.lean
@@ -3,12 +3,9 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Algebra.Algebra.Equiv
 import Mathlib.Algebra.Star.SelfAdjoint
 import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
-import Mathlib.LinearAlgebra.FreeModule.Basic
 import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
-import Mathlib.SetTheory.Cardinal.Arithmetic
 
 /-!
 # Quaternions
@@ -18,15 +15,18 @@ algebraic structures on `ℍ[R]`.
 
 ## Main definitions
 
-* `QuaternionAlgebra R a b`, `ℍ[R, a, b]` :
-  [quaternion algebra](https://en.wikipedia.org/wiki/Quaternion_algebra) with coefficients `a`, `b`
-* `Quaternion R`, `ℍ[R]` : the space of quaternions, a.k.a. `QuaternionAlgebra R (-1) (-1)`;
+* `QuaternionAlgebra R a b c`, `ℍ[R, a, b, c]` :
+  [Bourbaki, *Algebra I*][bourbaki1989] with coefficients `a`, `b`, `c`
+  (Many other references such as Wikipedia assume $\operatorname{char} R ≠ 2$ therefore one can
+  complete the square and WLOG assume $b = 0$.)
+* `Quaternion R`, `ℍ[R]` : the space of quaternions, a.k.a.
+  `QuaternionAlgebra R (-1) (0) (-1)`;
 * `Quaternion.normSq` : square of the norm of a quaternion;
 
 We also define the following algebraic structures on `ℍ[R]`:
 
-* `Ring ℍ[R, a, b]`, `StarRing ℍ[R, a, b]`, and `Algebra R ℍ[R, a, b]` : for any commutative ring
-  `R`;
+* `Ring ℍ[R, a, b, c]`, `StarRing ℍ[R, a, b, c]`, and `Algebra R ℍ[R, a, b, c]` :
+  for any commutative ring `R`;
 * `Ring ℍ[R]`, `StarRing ℍ[R]`, and `Algebra R ℍ[R]` : for any commutative ring `R`;
 * `IsDomain ℍ[R]` : for a linear ordered commutative ring `R`;
 * `DivisionRing ℍ[R]` : for a linear ordered field `R`.
@@ -35,7 +35,8 @@ We also define the following algebraic structures on `ℍ[R]`:
 
 The following notation is available with `open Quaternion` or `open scoped Quaternion`.
 
-* `ℍ[R, c₁, c₂]` : `QuaternionAlgebra R c₁ c₂`
+* `ℍ[R, c₁, c₂, c₃]` : `QuaternionAlgebra R c₁ c₂ c₃`
+* `ℍ[R, c₁, c₂]` : `QuaternionAlgebra R c₁ 0 c₂`
 * `ℍ[R]` : quaternions over `R`.
 
 ## Implementation notes
@@ -50,10 +51,10 @@ quaternion
 -/
 
 
-/-- Quaternion algebra over a type with fixed coefficients $a=i^2$ and $b=j^2$.
+/-- Quaternion algebra over a type with fixed coefficients where $i^2 = a + bi$ and $j^2 = c$.
 Implemented as a structure with four fields: `re`, `imI`, `imJ`, and `imK`. -/
 @[ext]
-structure QuaternionAlgebra (R : Type*) (a b : R) where
+structure QuaternionAlgebra (R : Type*) (a b c : R) where
   /-- Real part of a quaternion. -/
   re : R
   /-- First imaginary part (i) of a quaternion. -/
@@ -64,14 +65,18 @@ structure QuaternionAlgebra (R : Type*) (a b : R) where
   imK : R
 
 @[inherit_doc]
-scoped[Quaternion] notation "ℍ[" R "," a "," b "]" => QuaternionAlgebra R a b
-open Quaternion
+scoped[Quaternion] notation "ℍ[" R "," a "," b "," c "]" =>
+    QuaternionAlgebra R a b c
+
+@[inherit_doc]
+scoped[Quaternion] notation "ℍ[" R "," a "," b "]" => QuaternionAlgebra R a 0 b
 
 namespace QuaternionAlgebra
+open Quaternion
 
 /-- The equivalence between a quaternion algebra over `R` and `R × R × R × R`. -/
 @[simps]
-def equivProd {R : Type*} (c₁ c₂ : R) : ℍ[R,c₁,c₂] ≃ R × R × R × R where
+def equivProd {R : Type*} (c₁ c₂ c₃: R) : ℍ[R,c₁,c₂,c₃] ≃ R × R × R × R where
   toFun a := ⟨a.1, a.2, a.3, a.4⟩
   invFun a := ⟨a.1, a.2.1, a.2.2.1, a.2.2.2⟩
   left_inv _ := rfl
@@ -79,30 +84,34 @@ def equivProd {R : Type*} (c₁ c₂ : R) : ℍ[R,c₁,c₂] ≃ R × R × R ×
 
 /-- The equivalence between a quaternion algebra over `R` and `Fin 4 → R`. -/
 @[simps symm_apply]
-def equivTuple {R : Type*} (c₁ c₂ : R) : ℍ[R,c₁,c₂] ≃ (Fin 4 → R) where
+def equivTuple {R : Type*} (c₁ c₂ c₃: R) : ℍ[R,c₁,c₂,c₃] ≃ (Fin 4 → R) where
   toFun a := ![a.1, a.2, a.3, a.4]
   invFun a := ⟨a 0, a 1, a 2, a 3⟩
   left_inv _ := rfl
   right_inv f := by ext ⟨_, _ | _ | _ | _ | _ | ⟨⟩⟩ <;> rfl
 
 @[simp]
-theorem equivTuple_apply {R : Type*} (c₁ c₂ : R) (x : ℍ[R,c₁,c₂]) :
-    equivTuple c₁ c₂ x = ![x.re, x.imI, x.imJ, x.imK] :=
+theorem equivTuple_apply {R : Type*} (c₁ c₂ c₃: R) (x : ℍ[R,c₁,c₂,c₃]) :
+    equivTuple c₁ c₂ c₃ x = ![x.re, x.imI, x.imJ, x.imK] :=
   rfl
 
 @[simp]
-theorem mk.eta {R : Type*} {c₁ c₂} (a : ℍ[R,c₁,c₂]) : mk a.1 a.2 a.3 a.4 = a := rfl
+theorem mk.eta {R : Type*} {c₁ c₂ c₃} (a : ℍ[R,c₁,c₂,c₃]) : mk a.1 a.2 a.3 a.4 = a := rfl
 
-variable {S T R : Type*} {c₁ c₂ : R} (r x y : R) (a b : ℍ[R,c₁,c₂])
+variable {S T R : Type*} {c₁ c₂ c₃ : R} (r x y : R) (a b : ℍ[R,c₁,c₂,c₃])
 
-instance [Subsingleton R] : Subsingleton ℍ[R, c₁, c₂] := (equivTuple c₁ c₂).subsingleton
-instance [Nontrivial R] : Nontrivial ℍ[R, c₁, c₂] := (equivTuple c₁ c₂).surjective.nontrivial
+instance [Subsingleton R] : Subsingleton ℍ[R, c₁, c₂, c₃] := (equivTuple c₁ c₂ c₃).subsingleton
+instance [Nontrivial R] : Nontrivial ℍ[R, c₁, c₂, c₃] := (equivTuple c₁ c₂ c₃).surjective.nontrivial
 
 section Zero
 variable [Zero R]
 
-/-- The imaginary part of a quaternion. -/
-def im (x : ℍ[R,c₁,c₂]) : ℍ[R,c₁,c₂] :=
+/-- The imaginary part of a quaternion.
+
+Note that unless `c₂ = 0`, this definition is not particularly well-behaved;
+for instance, `QuaternionAlgebra.star_im` only says that the star of an imaginary quaternion
+is imaginary under this condition. -/
+def im (x : ℍ[R,c₁,c₂,c₃]) : ℍ[R,c₁,c₂,c₃] :=
   ⟨0, x.imI, x.imJ, x.imK⟩
 
 @[simp]
@@ -125,66 +134,66 @@ theorem im_imK : a.im.imK = a.imK :=
 theorem im_idem : a.im.im = a.im :=
   rfl
 
-/-- Coercion `R → ℍ[R,c₁,c₂]`. -/
-@[coe] def coe (x : R) : ℍ[R,c₁,c₂] := ⟨x, 0, 0, 0⟩
+/-- Coercion `R → ℍ[R,c₁,c₂,c₃]`. -/
+@[coe] def coe (x : R) : ℍ[R,c₁,c₂,c₃] := ⟨x, 0, 0, 0⟩
 
-instance : CoeTC R ℍ[R,c₁,c₂] := ⟨coe⟩
+instance : CoeTC R ℍ[R,c₁,c₂,c₃] := ⟨coe⟩
 
 @[simp, norm_cast]
-theorem coe_re : (x : ℍ[R,c₁,c₂]).re = x := rfl
+theorem coe_re : (x : ℍ[R,c₁,c₂,c₃]).re = x := rfl
 
 @[simp, norm_cast]
-theorem coe_imI : (x : ℍ[R,c₁,c₂]).imI = 0 := rfl
+theorem coe_imI : (x : ℍ[R,c₁,c₂,c₃]).imI = 0 := rfl
 
 @[simp, norm_cast]
-theorem coe_imJ : (x : ℍ[R,c₁,c₂]).imJ = 0 := rfl
+theorem coe_imJ : (x : ℍ[R,c₁,c₂,c₃]).imJ = 0 := rfl
 
 @[simp, norm_cast]
-theorem coe_imK : (x : ℍ[R,c₁,c₂]).imK = 0 := rfl
+theorem coe_imK : (x : ℍ[R,c₁,c₂,c₃]).imK = 0 := rfl
 
-theorem coe_injective : Function.Injective (coe : R → ℍ[R,c₁,c₂]) := fun _ _ h => congr_arg re h
+theorem coe_injective : Function.Injective (coe : R → ℍ[R,c₁,c₂,c₃]) := fun _ _ h => congr_arg re h
 
 @[simp]
-theorem coe_inj {x y : R} : (x : ℍ[R,c₁,c₂]) = y ↔ x = y :=
+theorem coe_inj {x y : R} : (x : ℍ[R,c₁,c₂,c₃]) = y ↔ x = y :=
   coe_injective.eq_iff
 
 -- Porting note: removed `simps`, added simp lemmas manually.
 -- Should adjust `simps` to name properly, i.e. as `zero_re` rather than `instZero_zero_re`.
-instance : Zero ℍ[R,c₁,c₂] := ⟨⟨0, 0, 0, 0⟩⟩
+instance : Zero ℍ[R,c₁,c₂,c₃] := ⟨⟨0, 0, 0, 0⟩⟩
 
-@[simp] theorem zero_re : (0 : ℍ[R,c₁,c₂]).re = 0 := rfl
+@[simp] theorem zero_re : (0 : ℍ[R,c₁,c₂,c₃]).re = 0 := rfl
 
-@[simp] theorem zero_imI : (0 : ℍ[R,c₁,c₂]).imI = 0 := rfl
+@[simp] theorem zero_imI : (0 : ℍ[R,c₁,c₂,c₃]).imI = 0 := rfl
 
-@[simp] theorem zero_imJ : (0 : ℍ[R,c₁,c₂]).imJ = 0 := rfl
+@[simp] theorem zero_imJ : (0 : ℍ[R,c₁,c₂,c₃]).imJ = 0 := rfl
 
-@[simp] theorem zero_imK : (0 : ℍ[R,c₁,c₂]).imK = 0 := rfl
+@[simp] theorem zero_imK : (0 : ℍ[R,c₁,c₂,c₃]).imK = 0 := rfl
 
-@[simp] theorem zero_im : (0 : ℍ[R,c₁,c₂]).im = 0 := rfl
+@[simp] theorem zero_im : (0 : ℍ[R,c₁,c₂,c₃]).im = 0 := rfl
 
 @[simp, norm_cast]
-theorem coe_zero : ((0 : R) : ℍ[R,c₁,c₂]) = 0 := rfl
+theorem coe_zero : ((0 : R) : ℍ[R,c₁,c₂,c₃]) = 0 := rfl
 
-instance : Inhabited ℍ[R,c₁,c₂] := ⟨0⟩
+instance : Inhabited ℍ[R,c₁,c₂,c₃] := ⟨0⟩
 
 section One
 variable [One R]
 
 -- Porting note: removed `simps`, added simp lemmas manually. Should adjust `simps` to name properly
-instance : One ℍ[R,c₁,c₂] := ⟨⟨1, 0, 0, 0⟩⟩
+instance : One ℍ[R,c₁,c₂,c₃] := ⟨⟨1, 0, 0, 0⟩⟩
 
-@[simp] theorem one_re : (1 : ℍ[R,c₁,c₂]).re = 1 := rfl
+@[simp] theorem one_re : (1 : ℍ[R,c₁,c₂,c₃]).re = 1 := rfl
 
-@[simp] theorem one_imI : (1 : ℍ[R,c₁,c₂]).imI = 0 := rfl
+@[simp] theorem one_imI : (1 : ℍ[R,c₁,c₂,c₃]).imI = 0 := rfl
 
-@[simp] theorem one_imJ : (1 : ℍ[R,c₁,c₂]).imJ = 0 := rfl
+@[simp] theorem one_imJ : (1 : ℍ[R,c₁,c₂,c₃]).imJ = 0 := rfl
 
-@[simp] theorem one_imK : (1 : ℍ[R,c₁,c₂]).imK = 0 := rfl
+@[simp] theorem one_imK : (1 : ℍ[R,c₁,c₂,c₃]).imK = 0 := rfl
 
-@[simp] theorem one_im : (1 : ℍ[R,c₁,c₂]).im = 0 := rfl
+@[simp] theorem one_im : (1 : ℍ[R,c₁,c₂,c₃]).im = 0 := rfl
 
 @[simp, norm_cast]
-theorem coe_one : ((1 : R) : ℍ[R,c₁,c₂]) = 1 := rfl
+theorem coe_one : ((1 : R) : ℍ[R,c₁,c₂,c₃]) = 1 := rfl
 
 end One
 end Zero
@@ -192,7 +201,7 @@ section Add
 variable [Add R]
 
 -- Porting note: removed `simps`, added simp lemmas manually. Should adjust `simps` to name properly
-instance : Add ℍ[R,c₁,c₂] :=
+instance : Add ℍ[R,c₁,c₂,c₃] :=
   ⟨fun a b => ⟨a.1 + b.1, a.2 + b.2, a.3 + b.3, a.4 + b.4⟩⟩
 
 @[simp] theorem add_re : (a + b).re = a.re + b.re := rfl
@@ -205,7 +214,8 @@ instance : Add ℍ[R,c₁,c₂] :=
 
 @[simp]
 theorem mk_add_mk (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) :
-    (mk a₁ a₂ a₃ a₄ : ℍ[R,c₁,c₂]) + mk b₁ b₂ b₃ b₄ = mk (a₁ + b₁) (a₂ + b₂) (a₃ + b₃) (a₄ + b₄) :=
+    (mk a₁ a₂ a₃ a₄ : ℍ[R,c₁,c₂,c₃]) + mk b₁ b₂ b₃ b₄ =
+    mk (a₁ + b₁) (a₂ + b₂) (a₃ + b₃) (a₄ + b₄) :=
   rfl
 
 end Add
@@ -217,7 +227,7 @@ variable [AddZeroClass R]
   QuaternionAlgebra.ext (zero_add _).symm rfl rfl rfl
 
 @[simp, norm_cast]
-theorem coe_add : ((x + y : R) : ℍ[R,c₁,c₂]) = x + y := by ext <;> simp
+theorem coe_add : ((x + y : R) : ℍ[R,c₁,c₂,c₃]) = x + y := by ext <;> simp
 
 end AddZeroClass
 
@@ -225,7 +235,7 @@ section Neg
 variable [Neg R]
 
 -- Porting note: removed `simps`, added simp lemmas manually. Should adjust `simps` to name properly
-instance : Neg ℍ[R,c₁,c₂] := ⟨fun a => ⟨-a.1, -a.2, -a.3, -a.4⟩⟩
+instance : Neg ℍ[R,c₁,c₂,c₃] := ⟨fun a => ⟨-a.1, -a.2, -a.3, -a.4⟩⟩
 
 @[simp] theorem neg_re : (-a).re = -a.re := rfl
 
@@ -236,7 +246,7 @@ instance : Neg ℍ[R,c₁,c₂] := ⟨fun a => ⟨-a.1, -a.2, -a.3, -a.4⟩⟩
 @[simp] theorem neg_imK : (-a).imK = -a.imK := rfl
 
 @[simp]
-theorem neg_mk (a₁ a₂ a₃ a₄ : R) : -(mk a₁ a₂ a₃ a₄ : ℍ[R,c₁,c₂]) = ⟨-a₁, -a₂, -a₃, -a₄⟩ :=
+theorem neg_mk (a₁ a₂ a₃ a₄ : R) : -(mk a₁ a₂ a₃ a₄ : ℍ[R,c₁,c₂,c₃]) = ⟨-a₁, -a₂, -a₃, -a₄⟩ :=
   rfl
 
 end Neg
@@ -248,9 +258,9 @@ variable [AddGroup R]
   QuaternionAlgebra.ext neg_zero.symm rfl rfl rfl
 
 @[simp, norm_cast]
-theorem coe_neg : ((-x : R) : ℍ[R,c₁,c₂]) = -x := by ext <;> simp
+theorem coe_neg : ((-x : R) : ℍ[R,c₁,c₂,c₃]) = -x := by ext <;> simp
 
-instance : Sub ℍ[R,c₁,c₂] :=
+instance : Sub ℍ[R,c₁,c₂,c₃] :=
   ⟨fun a b => ⟨a.1 - b.1, a.2 - b.2, a.3 - b.3, a.4 - b.4⟩⟩
 
 @[simp] theorem sub_re : (a - b).re = a.re - b.re := rfl
@@ -266,11 +276,12 @@ instance : Sub ℍ[R,c₁,c₂] :=
 
 @[simp]
 theorem mk_sub_mk (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) :
-    (mk a₁ a₂ a₃ a₄ : ℍ[R,c₁,c₂]) - mk b₁ b₂ b₃ b₄ = mk (a₁ - b₁) (a₂ - b₂) (a₃ - b₃) (a₄ - b₄) :=
+    (mk a₁ a₂ a₃ a₄ : ℍ[R,c₁,c₂,c₃]) - mk b₁ b₂ b₃ b₄ =
+    mk (a₁ - b₁) (a₂ - b₂) (a₃ - b₃) (a₄ - b₄) :=
   rfl
 
 @[simp, norm_cast]
-theorem coe_im : (x : ℍ[R,c₁,c₂]).im = 0 :=
+theorem coe_im : (x : ℍ[R,c₁,c₂,c₃]).im = 0 :=
   rfl
 
 @[simp]
@@ -293,37 +304,43 @@ variable [Ring R]
 /-- Multiplication is given by
 
 * `1 * x = x * 1 = x`;
-* `i * i = c₁`;
-* `j * j = c₂`;
-* `i * j = k`, `j * i = -k`;
-* `k * k = -c₁ * c₂`;
-* `i * k = c₁ * j`, `k * i = -c₁ * j`;
-* `j * k = -c₂ * i`, `k * j = c₂ * i`. -/
-instance : Mul ℍ[R,c₁,c₂] :=
+* `i * i = c₁ + c₂ * i`;
+* `j * j = c₃`;
+* `i * j = k`, `j * i = c₂ * j - k`;
+* `k * k = - c₁ * c₃`;
+* `i * k = c₁ * j + c₂ * k`, `k * i = -c₁ * j`;
+* `j * k = c₂ * c₃ - c₃ * i`, `k * j = c₃ * i`. -/
+instance : Mul ℍ[R,c₁,c₂,c₃] :=
   ⟨fun a b =>
-    ⟨a.1 * b.1 + c₁ * a.2 * b.2 + c₂ * a.3 * b.3 - c₁ * c₂ * a.4 * b.4,
-      a.1 * b.2 + a.2 * b.1 - c₂ * a.3 * b.4 + c₂ * a.4 * b.3,
-      a.1 * b.3 + c₁ * a.2 * b.4 + a.3 * b.1 - c₁ * a.4 * b.2,
-      a.1 * b.4 + a.2 * b.3 - a.3 * b.2 + a.4 * b.1⟩⟩
+    ⟨a.1 * b.1 + c₁ * a.2 * b.2 + c₃ * a.3 * b.3 + c₂ * c₃ * a.3 * b.4 - c₁ * c₃ * a.4 * b.4,
+      a.1 * b.2 + a.2 * b.1 + c₂ * a.2 * b.2 - c₃ * a.3 * b.4 + c₃ * a.4 * b.3,
+      a.1 * b.3 + c₁ * a.2 * b.4 + a.3 * b.1 + c₂ * a.3 * b.2 - c₁ * a.4 * b.2,
+      a.1 * b.4 + a.2 * b.3 + c₂ * a.2 * b.4 - a.3 * b.2 + a.4 * b.1⟩⟩
 
 @[simp]
-theorem mul_re : (a * b).re = a.1 * b.1 + c₁ * a.2 * b.2 + c₂ * a.3 * b.3 - c₁ * c₂ * a.4 * b.4 :=
-  rfl
+theorem mul_re : (a * b).re = a.1 * b.1 + c₁ * a.2 * b.2 + c₃ * a.3 * b.3 +
+    c₂ * c₃ * a.3 * b.4 - c₁ * c₃ * a.4 * b.4 := rfl
 
 @[simp]
-theorem mul_imI : (a * b).imI = a.1 * b.2 + a.2 * b.1 - c₂ * a.3 * b.4 + c₂ * a.4 * b.3 := rfl
+theorem mul_imI : (a * b).imI = a.1 * b.2 + a.2 * b.1 +
+    c₂ * a.2 * b.2 - c₃ * a.3 * b.4 + c₃ * a.4 * b.3 := rfl
 
 @[simp]
-theorem mul_imJ : (a * b).imJ = a.1 * b.3 + c₁ * a.2 * b.4 + a.3 * b.1 - c₁ * a.4 * b.2 := rfl
+theorem mul_imJ : (a * b).imJ = a.1 * b.3 + c₁ * a.2 * b.4 + a.3 * b.1 +
+    c₂ * a.3 * b.2 - c₁ * a.4 * b.2 := rfl
 
-@[simp] theorem mul_imK : (a * b).imK = a.1 * b.4 + a.2 * b.3 - a.3 * b.2 + a.4 * b.1 := rfl
+@[simp]
+theorem mul_imK : (a * b).imK = a.1 * b.4 + a.2 * b.3 +
+    c₂ * a.2 * b.4 - a.3 * b.2 + a.4 * b.1 := rfl
 
 @[simp]
 theorem mk_mul_mk (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) :
-    (mk a₁ a₂ a₃ a₄ : ℍ[R,c₁,c₂]) * mk b₁ b₂ b₃ b₄ =
-      ⟨a₁ * b₁ + c₁ * a₂ * b₂ + c₂ * a₃ * b₃ - c₁ * c₂ * a₄ * b₄,
-        a₁ * b₂ + a₂ * b₁ - c₂ * a₃ * b₄ + c₂ * a₄ * b₃,
-        a₁ * b₃ + c₁ * a₂ * b₄ + a₃ * b₁ - c₁ * a₄ * b₂, a₁ * b₄ + a₂ * b₃ - a₃ * b₂ + a₄ * b₁⟩ :=
+    (mk a₁ a₂ a₃ a₄ : ℍ[R,c₁,c₂,c₃]) * mk b₁ b₂ b₃ b₄ =
+    mk
+      (a₁ * b₁ + c₁ * a₂ * b₂ + c₃ * a₃ * b₃ + c₂ * c₃ * a₃ * b₄ - c₁ * c₃ * a₄ * b₄)
+      (a₁ * b₂ + a₂ * b₁ + c₂ * a₂ * b₂ - c₃ * a₃ * b₄ + c₃ * a₄ * b₃)
+      (a₁ * b₃ + c₁ * a₂ * b₄ + a₃ * b₁ + c₂ * a₃ * b₂ - c₁ * a₄ * b₂)
+      (a₁ * b₄ + a₂ * b₃ + c₂ * a₂ * b₄ - a₃ * b₂ + a₄ * b₁) :=
   rfl
 
 end Ring
@@ -331,12 +348,12 @@ section SMul
 
 variable [SMul S R] [SMul T R] (s : S)
 
-instance : SMul S ℍ[R,c₁,c₂] where smul s a := ⟨s • a.1, s • a.2, s • a.3, s • a.4⟩
+instance : SMul S ℍ[R,c₁,c₂,c₃] where smul s a := ⟨s • a.1, s • a.2, s • a.3, s • a.4⟩
 
-instance [SMul S T] [IsScalarTower S T R] : IsScalarTower S T ℍ[R,c₁,c₂] where
+instance [SMul S T] [IsScalarTower S T R] : IsScalarTower S T ℍ[R,c₁,c₂,c₃] where
   smul_assoc s t x := by ext <;> exact smul_assoc _ _ _
 
-instance [SMulCommClass S T R] : SMulCommClass S T ℍ[R,c₁,c₂] where
+instance [SMulCommClass S T R] : SMulCommClass S T ℍ[R,c₁,c₂,c₃] where
   smul_comm s t x := by ext <;> exact smul_comm _ _ _
 
 @[simp] theorem smul_re : (s • a).re = s • a.re := rfl
@@ -352,112 +369,127 @@ instance [SMulCommClass S T R] : SMulCommClass S T ℍ[R,c₁,c₂] where
 
 @[simp]
 theorem smul_mk (re im_i im_j im_k : R) :
-    s • (⟨re, im_i, im_j, im_k⟩ : ℍ[R,c₁,c₂]) = ⟨s • re, s • im_i, s • im_j, s • im_k⟩ :=
+    s • (⟨re, im_i, im_j, im_k⟩ : ℍ[R,c₁,c₂,c₃]) = ⟨s • re, s • im_i, s • im_j, s • im_k⟩ :=
   rfl
 
 end SMul
 
 @[simp, norm_cast]
 theorem coe_smul [Zero R] [SMulZeroClass S R] (s : S) (r : R) :
-    (↑(s • r) : ℍ[R,c₁,c₂]) = s • (r : ℍ[R,c₁,c₂]) :=
-  QuaternionAlgebra.ext rfl (smul_zero s).symm (smul_zero s).symm (smul_zero s).symm
+    (↑(s • r) : ℍ[R,c₁,c₂,c₃]) = s • (r : ℍ[R,c₁,c₂,c₃]) :=
+  QuaternionAlgebra.ext rfl (smul_zero _).symm (smul_zero _).symm (smul_zero _).symm
 
-instance [AddCommGroup R] : AddCommGroup ℍ[R,c₁,c₂] :=
-  (equivProd c₁ c₂).injective.addCommGroup _ rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl)
+instance [AddCommGroup R] : AddCommGroup ℍ[R,c₁,c₂,c₃] :=
+  (equivProd c₁ c₂ c₃).injective.addCommGroup _ rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl)
     (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
 
 section AddCommGroupWithOne
 variable [AddCommGroupWithOne R]
 
-instance : AddCommGroupWithOne ℍ[R,c₁,c₂] where
-  natCast n := ((n : R) : ℍ[R,c₁,c₂])
+instance : AddCommGroupWithOne ℍ[R,c₁,c₂,c₃] where
+  natCast n := ((n : R) : ℍ[R,c₁,c₂,c₃])
   natCast_zero := by simp
   natCast_succ := by simp
-  intCast n := ((n : R) : ℍ[R,c₁,c₂])
+  intCast n := ((n : R) : ℍ[R,c₁,c₂,c₃])
   intCast_ofNat _ := congr_arg coe (Int.cast_natCast _)
   intCast_negSucc n := by
     change coe _ = -coe _
     rw [Int.cast_negSucc, coe_neg]
 
 @[simp, norm_cast]
-theorem natCast_re (n : ℕ) : (n : ℍ[R,c₁,c₂]).re = n :=
+theorem natCast_re (n : ℕ) : (n : ℍ[R,c₁,c₂,c₃]).re = n :=
   rfl
 
 @[deprecated (since := "2024-04-17")]
 alias nat_cast_re := natCast_re
 
 @[simp, norm_cast]
-theorem natCast_imI (n : ℕ) : (n : ℍ[R,c₁,c₂]).imI = 0 :=
+theorem natCast_imI (n : ℕ) : (n : ℍ[R,c₁,c₂,c₃]).imI = 0 :=
   rfl
 
 @[deprecated (since := "2024-04-17")]
 alias nat_cast_imI := natCast_imI
 
 @[simp, norm_cast]
-theorem natCast_imJ (n : ℕ) : (n : ℍ[R,c₁,c₂]).imJ = 0 :=
+theorem natCast_imJ (n : ℕ) : (n : ℍ[R,c₁,c₂,c₃]).imJ = 0 :=
   rfl
 
 @[deprecated (since := "2024-04-17")]
 alias nat_cast_imJ := natCast_imJ
 
 @[simp, norm_cast]
-theorem natCast_imK (n : ℕ) : (n : ℍ[R,c₁,c₂]).imK = 0 :=
+theorem natCast_imK (n : ℕ) : (n : ℍ[R,c₁,c₂,c₃]).imK = 0 :=
   rfl
 
 @[deprecated (since := "2024-04-17")]
 alias nat_cast_imK := natCast_imK
 
 @[simp, norm_cast]
-theorem natCast_im (n : ℕ) : (n : ℍ[R,c₁,c₂]).im = 0 :=
+theorem natCast_im (n : ℕ) : (n : ℍ[R,c₁,c₂,c₃]).im = 0 :=
   rfl
 
 @[deprecated (since := "2024-04-17")]
 alias nat_cast_im := natCast_im
 
 @[norm_cast]
-theorem coe_natCast (n : ℕ) : ↑(n : R) = (n : ℍ[R,c₁,c₂]) :=
+theorem coe_natCast (n : ℕ) : ↑(n : R) = (n : ℍ[R,c₁,c₂,c₃]) :=
   rfl
 
 @[deprecated (since := "2024-04-17")]
 alias coe_nat_cast := coe_natCast
 
 @[simp, norm_cast]
-theorem intCast_re (z : ℤ) : (z : ℍ[R,c₁,c₂]).re = z :=
+theorem intCast_re (z : ℤ) : (z : ℍ[R,c₁,c₂,c₃]).re = z :=
   rfl
 
+@[simp]
+theorem ofNat_re (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : ℍ[R,c₁,c₂,c₃]).re = ofNat(n) := rfl
+
+@[simp]
+theorem ofNat_imI (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : ℍ[R,c₁,c₂,c₃]).imI = 0 := rfl
+
+@[simp]
+theorem ofNat_imJ (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : ℍ[R,c₁,c₂,c₃]).imJ = 0 := rfl
+
+@[simp]
+theorem ofNat_imK (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : ℍ[R,c₁,c₂,c₃]).imK = 0 := rfl
+
+@[simp]
+theorem ofNat_im (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : ℍ[R,c₁,c₂,c₃]).im = 0 := rfl
+
 @[deprecated (since := "2024-04-17")]
 alias int_cast_re := intCast_re
 
 @[simp, norm_cast]
-theorem intCast_imI (z : ℤ) : (z : ℍ[R,c₁,c₂]).imI = 0 :=
+theorem intCast_imI (z : ℤ) : (z : ℍ[R,c₁,c₂,c₃]).imI = 0 :=
   rfl
 
 @[deprecated (since := "2024-04-17")]
 alias int_cast_imI := intCast_imI
 
 @[simp, norm_cast]
-theorem intCast_imJ (z : ℤ) : (z : ℍ[R,c₁,c₂]).imJ = 0 :=
+theorem intCast_imJ (z : ℤ) : (z : ℍ[R,c₁,c₂,c₃]).imJ = 0 :=
   rfl
 
 @[deprecated (since := "2024-04-17")]
 alias int_cast_imJ := intCast_imJ
 
 @[simp, norm_cast]
-theorem intCast_imK (z : ℤ) : (z : ℍ[R,c₁,c₂]).imK = 0 :=
+theorem intCast_imK (z : ℤ) : (z : ℍ[R,c₁,c₂,c₃]).imK = 0 :=
   rfl
 
 @[deprecated (since := "2024-04-17")]
 alias int_cast_imK := intCast_imK
 
 @[simp, norm_cast]
-theorem intCast_im (z : ℤ) : (z : ℍ[R,c₁,c₂]).im = 0 :=
+theorem intCast_im (z : ℤ) : (z : ℍ[R,c₁,c₂,c₃]).im = 0 :=
   rfl
 
 @[deprecated (since := "2024-04-17")]
 alias int_cast_im := intCast_im
 
 @[norm_cast]
-theorem coe_intCast (z : ℤ) : ↑(z : R) = (z : ℍ[R,c₁,c₂]) :=
+theorem coe_intCast (z : ℤ) : ↑(z : R) = (z : ℍ[R,c₁,c₂,c₃]) :=
   rfl
 
 @[deprecated (since := "2024-04-17")]
@@ -468,8 +500,8 @@ end AddCommGroupWithOne
 -- For the remainder of the file we assume `CommRing R`.
 variable [CommRing R]
 
-instance instRing : Ring ℍ[R,c₁,c₂] where
-  __ := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂])
+instance instRing : Ring ℍ[R,c₁,c₂,c₃] where
+  __ := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂,c₃])
   left_distrib _ _ _ := by ext <;> simp <;> ring
   right_distrib _ _ _ := by ext <;> simp <;> ring
   zero_mul _ := by ext <;> simp
@@ -479,11 +511,16 @@ instance instRing : Ring ℍ[R,c₁,c₂] where
   mul_one _ := by ext <;> simp
 
 @[norm_cast, simp]
-theorem coe_mul : ((x * y : R) : ℍ[R,c₁,c₂]) = x * y := by ext <;> simp
+theorem coe_mul : ((x * y : R) : ℍ[R,c₁,c₂,c₃]) = x * y := by ext <;> simp
+
+@[norm_cast, simp]
+lemma coe_ofNat {n : ℕ} [n.AtLeastTwo]:
+    ((ofNat(n) : R) : ℍ[R,c₁,c₂,c₃]) = (ofNat(n) : ℍ[R,c₁,c₂,c₃]) := by
+  rfl
 
 -- TODO: add weaker `MulAction`, `DistribMulAction`, and `Module` instances (and repeat them
 -- for `ℍ[R]`)
-instance [CommSemiring S] [Algebra S R] : Algebra S ℍ[R,c₁,c₂] where
+instance [CommSemiring S] [Algebra S R] : Algebra S ℍ[R,c₁,c₂,c₃] where
   smul := (· • ·)
   algebraMap :=
   { toFun s := coe (algebraMap S R s)
@@ -494,13 +531,13 @@ instance [CommSemiring S] [Algebra S R] : Algebra S ℍ[R,c₁,c₂] where
   smul_def' s x := by ext <;> simp [Algebra.smul_def]
   commutes' s x := by ext <;> simp [Algebra.commutes]
 
-theorem algebraMap_eq (r : R) : algebraMap R ℍ[R,c₁,c₂] r = ⟨r, 0, 0, 0⟩ :=
+theorem algebraMap_eq (r : R) : algebraMap R ℍ[R,c₁,c₂,c₃] r = ⟨r, 0, 0, 0⟩ :=
   rfl
 
-theorem algebraMap_injective : (algebraMap R ℍ[R,c₁,c₂] : _ → _).Injective :=
+theorem algebraMap_injective : (algebraMap R ℍ[R,c₁,c₂,c₃] : _ → _).Injective :=
   fun _ _ ↦ by simp [algebraMap_eq]
 
-instance [NoZeroDivisors R] : NoZeroSMulDivisors R ℍ[R,c₁,c₂] := ⟨by
+instance [NoZeroDivisors R] : NoZeroSMulDivisors R ℍ[R,c₁,c₂,c₃] := ⟨by
   rintro t ⟨a, b, c, d⟩ h
   rw [or_iff_not_imp_left]
   intro ht
@@ -508,97 +545,94 @@ instance [NoZeroDivisors R] : NoZeroSMulDivisors R ℍ[R,c₁,c₂] := ⟨by
 
 section
 
-variable (c₁ c₂)
+variable (c₁ c₂ c₃)
 
 /-- `QuaternionAlgebra.re` as a `LinearMap`-/
 @[simps]
-def reₗ : ℍ[R,c₁,c₂] →ₗ[R] R where
+def reₗ : ℍ[R,c₁,c₂,c₃] →ₗ[R] R where
   toFun := re
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
 
 /-- `QuaternionAlgebra.imI` as a `LinearMap`-/
 @[simps]
-def imIₗ : ℍ[R,c₁,c₂] →ₗ[R] R where
+def imIₗ : ℍ[R,c₁,c₂,c₃] →ₗ[R] R where
   toFun := imI
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
 
 /-- `QuaternionAlgebra.imJ` as a `LinearMap`-/
 @[simps]
-def imJₗ : ℍ[R,c₁,c₂] →ₗ[R] R where
+def imJₗ : ℍ[R,c₁,c₂,c₃] →ₗ[R] R where
   toFun := imJ
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
 
 /-- `QuaternionAlgebra.imK` as a `LinearMap`-/
 @[simps]
-def imKₗ : ℍ[R,c₁,c₂] →ₗ[R] R where
+def imKₗ : ℍ[R,c₁,c₂,c₃] →ₗ[R] R where
   toFun := imK
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
 
 /-- `QuaternionAlgebra.equivTuple` as a linear equivalence. -/
-def linearEquivTuple : ℍ[R,c₁,c₂] ≃ₗ[R] Fin 4 → R :=
+def linearEquivTuple : ℍ[R,c₁,c₂,c₃] ≃ₗ[R] Fin 4 → R :=
   LinearEquiv.symm -- proofs are not `rfl` in the forward direction
-    { (equivTuple c₁ c₂).symm with
-      toFun := (equivTuple c₁ c₂).symm
-      invFun := equivTuple c₁ c₂
+    { (equivTuple c₁ c₂ c₃).symm with
+      toFun := (equivTuple c₁ c₂ c₃).symm
+      invFun := equivTuple c₁ c₂ c₃
       map_add' := fun _ _ => rfl
       map_smul' := fun _ _ => rfl }
 
 @[simp]
-theorem coe_linearEquivTuple : ⇑(linearEquivTuple c₁ c₂) = equivTuple c₁ c₂ :=
-  rfl
+theorem coe_linearEquivTuple :
+    ⇑(linearEquivTuple c₁ c₂ c₃) = equivTuple c₁ c₂ c₃ := rfl
 
 @[simp]
-theorem coe_linearEquivTuple_symm : ⇑(linearEquivTuple c₁ c₂).symm = (equivTuple c₁ c₂).symm :=
-  rfl
+theorem coe_linearEquivTuple_symm :
+    ⇑(linearEquivTuple c₁ c₂ c₃).symm = (equivTuple c₁ c₂ c₃).symm := rfl
 
-/-- `ℍ[R, c₁, c₂]` has a basis over `R` given by `1`, `i`, `j`, and `k`. -/
-noncomputable def basisOneIJK : Basis (Fin 4) R ℍ[R,c₁,c₂] :=
-  .ofEquivFun <| linearEquivTuple c₁ c₂
+/-- `ℍ[R, c₁, c₂, c₃]` has a basis over `R` given by `1`, `i`, `j`, and `k`. -/
+noncomputable def basisOneIJK : Basis (Fin 4) R ℍ[R,c₁,c₂,c₃] :=
+  .ofEquivFun <| linearEquivTuple c₁ c₂ c₃
 
 @[simp]
-theorem coe_basisOneIJK_repr (q : ℍ[R,c₁,c₂]) :
-    ⇑((basisOneIJK c₁ c₂).repr q) = ![q.re, q.imI, q.imJ, q.imK] :=
+theorem coe_basisOneIJK_repr (q : ℍ[R,c₁,c₂,c₃]) :
+    ((basisOneIJK c₁ c₂ c₃).repr q) = ![q.re, q.imI, q.imJ, q.imK] :=
   rfl
 
-instance : Module.Finite R ℍ[R,c₁,c₂] := .of_basis (basisOneIJK c₁ c₂)
+instance : Module.Finite R ℍ[R,c₁,c₂,c₃] := .of_basis (basisOneIJK c₁ c₂ c₃)
 
-instance : Module.Free R ℍ[R,c₁,c₂] := .of_basis (basisOneIJK c₁ c₂)
+instance : Module.Free R ℍ[R,c₁,c₂,c₃] := .of_basis (basisOneIJK c₁ c₂ c₃)
 
-theorem rank_eq_four [StrongRankCondition R] : Module.rank R ℍ[R,c₁,c₂] = 4 := by
-  rw [rank_eq_card_basis (basisOneIJK c₁ c₂), Fintype.card_fin]
+theorem rank_eq_four [StrongRankCondition R] : Module.rank R ℍ[R,c₁,c₂,c₃] = 4 := by
+  rw [rank_eq_card_basis (basisOneIJK c₁ c₂ c₃), Fintype.card_fin]
   norm_num
 
-theorem finrank_eq_four [StrongRankCondition R] : Module.finrank R ℍ[R,c₁,c₂] = 4 := by
+theorem finrank_eq_four [StrongRankCondition R] : Module.finrank R ℍ[R,c₁,c₂,c₃] = 4 := by
   rw [Module.finrank, rank_eq_four, Cardinal.toNat_ofNat]
 
-/-- There is a natural equivalence when swapping the coefficients of a quaternion algebra. -/
+/-- There is a natural equivalence when swapping the first and third coefficients of a
+  quaternion algebra if `c₂` is 0. -/
 @[simps]
-def swapEquiv : ℍ[R,c₁,c₂] ≃ₐ[R] ℍ[R, c₂, c₁] where
+def swapEquiv : ℍ[R,c₁,0,c₃] ≃ₐ[R] ℍ[R,c₃,0,c₁] where
   toFun t := ⟨t.1, t.3, t.2, -t.4⟩
   invFun t := ⟨t.1, t.3, t.2, -t.4⟩
   left_inv _ := by simp
   right_inv _ := by simp
-  map_mul' _ _ := by
-    ext
-      <;> simp only [mul_re, mul_imJ, mul_imI, add_left_inj, mul_imK, neg_mul, neg_add_rev,
-                     neg_sub, mk_mul_mk, mul_neg, neg_neg, sub_neg_eq_add]
-      <;> ring
+  map_mul' _ _ := by ext <;> simp <;> ring
   map_add' _ _ := by ext <;> simp [add_comm]
   commutes' _ := by simp [algebraMap_eq]
 
 end
 
 @[norm_cast, simp]
-theorem coe_sub : ((x - y : R) : ℍ[R,c₁,c₂]) = x - y :=
-  (algebraMap R ℍ[R,c₁,c₂]).map_sub x y
+theorem coe_sub : ((x - y : R) : ℍ[R,c₁,c₂,c₃]) = x - y :=
+  (algebraMap R ℍ[R,c₁,c₂,c₃]).map_sub x y
 
 @[norm_cast, simp]
-theorem coe_pow (n : ℕ) : (↑(x ^ n) : ℍ[R,c₁,c₂]) = (x : ℍ[R,c₁,c₂]) ^ n :=
-  (algebraMap R ℍ[R,c₁,c₂]).map_pow x n
+theorem coe_pow (n : ℕ) : (↑(x ^ n) : ℍ[R,c₁,c₂,c₃]) = (x : ℍ[R,c₁,c₂,c₃]) ^ n :=
+  (algebraMap R ℍ[R,c₁,c₂,c₃]).map_pow x n
 
 theorem coe_commutes : ↑r * a = a * r :=
   Algebra.commutes r a
@@ -612,15 +646,16 @@ theorem coe_mul_eq_smul : ↑r * a = r • a :=
 theorem mul_coe_eq_smul : a * r = r • a := by rw [← coe_commutes, coe_mul_eq_smul]
 
 @[norm_cast, simp]
-theorem coe_algebraMap : ⇑(algebraMap R ℍ[R,c₁,c₂]) = coe :=
+theorem coe_algebraMap : ⇑(algebraMap R ℍ[R,c₁,c₂,c₃]) = coe :=
   rfl
 
-theorem smul_coe : x • (y : ℍ[R,c₁,c₂]) = ↑(x * y) := by rw [coe_mul, coe_mul_eq_smul]
+theorem smul_coe : x • (y : ℍ[R,c₁,c₂,c₃]) = ↑(x * y) := by rw [coe_mul, coe_mul_eq_smul]
 
 /-- Quaternion conjugate. -/
-instance instStarQuaternionAlgebra : Star ℍ[R,c₁,c₂] where star a := ⟨a.1, -a.2, -a.3, -a.4⟩
+instance instStarQuaternionAlgebra : Star ℍ[R,c₁,c₂,c₃] where star a :=
+  ⟨a.1 + c₂ * a.2, -a.2, -a.3, -a.4⟩
 
-@[simp] theorem re_star : (star a).re = a.re := rfl
+@[simp] theorem re_star : (star a).re = a.re + c₂ * a.imI := rfl
 
 @[simp]
 theorem imI_star : (star a).imI = -a.imI :=
@@ -639,44 +674,54 @@ theorem im_star : (star a).im = -a.im :=
   QuaternionAlgebra.ext neg_zero.symm rfl rfl rfl
 
 @[simp]
-theorem star_mk (a₁ a₂ a₃ a₄ : R) : star (mk a₁ a₂ a₃ a₄ : ℍ[R,c₁,c₂]) = ⟨a₁, -a₂, -a₃, -a₄⟩ :=
-  rfl
+theorem star_mk (a₁ a₂ a₃ a₄ : R) : star (mk a₁ a₂ a₃ a₄ : ℍ[R,c₁,c₂,c₃]) =
+    ⟨a₁ + c₂ * a₂, -a₂, -a₃, -a₄⟩ := rfl
 
-instance instStarRing : StarRing ℍ[R,c₁,c₂] where
+instance instStarRing : StarRing ℍ[R,c₁,c₂,c₃] where
   star_involutive x := by simp [Star.star]
-  star_add a b := by ext <;> simp [add_comm]
+  star_add a b := by ext <;> simp [add_comm] ; ring
   star_mul a b := by ext <;> simp <;> ring
 
-theorem self_add_star' : a + star a = ↑(2 * a.re) := by ext <;> simp [two_mul]
+theorem self_add_star' : a + star a = ↑(2 * a.re + c₂ * a.imI) := by ext <;> simp [two_mul]; ring
 
-theorem self_add_star : a + star a = 2 * a.re := by simp only [self_add_star', two_mul, coe_add]
+theorem self_add_star : a + star a = 2 * a.re + c₂ * a.imI := by simp [self_add_star']
 
-theorem star_add_self' : star a + a = ↑(2 * a.re) := by rw [add_comm, self_add_star']
+theorem star_add_self' : star a + a = ↑(2 * a.re + c₂ * a.imI) := by rw [add_comm, self_add_star']
 
-theorem star_add_self : star a + a = 2 * a.re := by rw [add_comm, self_add_star]
+theorem star_add_self : star a + a = 2 * a.re + c₂ * a.imI := by rw [add_comm, self_add_star]
 
-theorem star_eq_two_re_sub : star a = ↑(2 * a.re) - a :=
+theorem star_eq_two_re_sub : star a = ↑(2 * a.re + c₂ * a.imI) - a :=
   eq_sub_iff_add_eq.2 a.star_add_self'
 
+lemma comm (r : R) (x : ℍ[R, c₁, c₂, c₃]) : r * x = x * r := by
+  ext <;> simp [mul_comm]
+
 instance : IsStarNormal a :=
   ⟨by
-    rw [a.star_eq_two_re_sub]
-    exact (coe_commute (2 * a.re) a).sub_left (Commute.refl a)⟩
+    rw [commute_iff_eq, a.star_eq_two_re_sub];
+    ext <;> simp <;> ring⟩
 
 @[simp, norm_cast]
-theorem star_coe : star (x : ℍ[R,c₁,c₂]) = x := by ext <;> simp
+theorem star_coe : star (x : ℍ[R,c₁,c₂,c₃]) = x := by ext <;> simp
 
-@[simp] theorem star_im : star a.im = -a.im := im_star _
+@[simp] theorem star_im : star a.im = -a.im + c₂ * a.imI := by ext <;> simp
 
 @[simp]
-theorem star_smul [Monoid S] [DistribMulAction S R] (s : S) (a : ℍ[R,c₁,c₂]) :
+theorem star_smul [Monoid S] [DistribMulAction S R] [SMulCommClass S R R]
+    (s : S) (a : ℍ[R,c₁,c₂,c₃]) :
+    star (s • a) = s • star a :=
+  QuaternionAlgebra.ext
+    (by simp [mul_smul_comm]) (smul_neg _ _).symm (smul_neg _ _).symm (smul_neg _ _).symm
+
+/-- A version of `star_smul` for the special case when `c₂ = 0`, without `SMulCommClass S R R`. -/
+theorem star_smul' [Monoid S] [DistribMulAction S R] (s : S) (a : ℍ[R,c₁,0,c₃]) :
     star (s • a) = s • star a :=
-  QuaternionAlgebra.ext rfl (smul_neg _ _).symm (smul_neg _ _).symm (smul_neg _ _).symm
+  QuaternionAlgebra.ext (by simp) (smul_neg _ _).symm (smul_neg _ _).symm (smul_neg _ _).symm
 
-theorem eq_re_of_eq_coe {a : ℍ[R,c₁,c₂]} {x : R} (h : a = x) : a = a.re := by rw [h, coe_re]
+theorem eq_re_of_eq_coe {a : ℍ[R,c₁,c₂,c₃]} {x : R} (h : a = x) : a = a.re := by rw [h, coe_re]
 
-theorem eq_re_iff_mem_range_coe {a : ℍ[R,c₁,c₂]} :
-    a = a.re ↔ a ∈ Set.range (coe : R → ℍ[R,c₁,c₂]) :=
+theorem eq_re_iff_mem_range_coe {a : ℍ[R,c₁,c₂,c₃]} :
+    a = a.re ↔ a ∈ Set.range (coe : R → ℍ[R,c₁,c₂,c₃]) :=
   ⟨fun h => ⟨a.re, h.symm⟩, fun ⟨_, h⟩ => eq_re_of_eq_coe h.symm⟩
 
 section CharZero
@@ -684,10 +729,10 @@ section CharZero
 variable [NoZeroDivisors R] [CharZero R]
 
 @[simp]
-theorem star_eq_self {c₁ c₂ : R} {a : ℍ[R,c₁,c₂]} : star a = a ↔ a = a.re := by
-  simp [QuaternionAlgebra.ext_iff, neg_eq_iff_add_eq_zero, add_self_eq_zero]
+theorem star_eq_self {c₁ c₂ : R} {a : ℍ[R,c₁,c₂,c₃]} : star a = a ↔ a = a.re := by
+  simp_all [QuaternionAlgebra.ext_iff, neg_eq_iff_add_eq_zero, add_self_eq_zero]
 
-theorem star_eq_neg {c₁ c₂ : R} {a : ℍ[R,c₁,c₂]} : star a = -a ↔ a.re = 0 := by
+theorem star_eq_neg {c₁ : R} {a : ℍ[R,c₁,0,c₃]} : star a = -a ↔ a.re = 0 := by
   simp [QuaternionAlgebra.ext_iff, eq_neg_iff_add_eq_zero]
 
 end CharZero
@@ -702,7 +747,7 @@ theorem mul_star_eq_coe : a * star a = (a * star a).re := by
 open MulOpposite
 
 /-- Quaternion conjugate as an `AlgEquiv` to the opposite ring. -/
-def starAe : ℍ[R,c₁,c₂] ≃ₐ[R] ℍ[R,c₁,c₂]ᵐᵒᵖ :=
+def starAe : ℍ[R,c₁,c₂,c₃] ≃ₐ[R] ℍ[R,c₁,c₂,c₃]ᵐᵒᵖ :=
   { starAddEquiv.trans opAddEquiv with
     toFun := op ∘ star
     invFun := star ∘ unop
@@ -710,38 +755,40 @@ def starAe : ℍ[R,c₁,c₂] ≃ₐ[R] ℍ[R,c₁,c₂]ᵐᵒᵖ :=
     commutes' := fun r => by simp }
 
 @[simp]
-theorem coe_starAe : ⇑(starAe : ℍ[R,c₁,c₂] ≃ₐ[R] _) = op ∘ star :=
+theorem coe_starAe : ⇑(starAe : ℍ[R,c₁,c₂,c₃] ≃ₐ[R] _) = op ∘ star :=
   rfl
 
 end QuaternionAlgebra
 
 /-- Space of quaternions over a type. Implemented as a structure with four fields:
 `re`, `im_i`, `im_j`, and `im_k`. -/
-def Quaternion (R : Type*) [One R] [Neg R] :=
-  QuaternionAlgebra R (-1) (-1)
+def Quaternion (R : Type*) [Zero R] [One R] [Neg R] :=
+  QuaternionAlgebra R (-1) (0) (-1)
 
 @[inherit_doc]
 scoped[Quaternion] notation "ℍ[" R "]" => Quaternion R
 
+open Quaternion
+
 /-- The equivalence between the quaternions over `R` and `R × R × R × R`. -/
 @[simps!]
-def Quaternion.equivProd (R : Type*) [One R] [Neg R] : ℍ[R] ≃ R × R × R × R :=
-  QuaternionAlgebra.equivProd _ _
+def Quaternion.equivProd (R : Type*) [Zero R] [One R] [Neg R] : ℍ[R] ≃ R × R × R × R :=
+  QuaternionAlgebra.equivProd _ _ _
 
 /-- The equivalence between the quaternions over `R` and `Fin 4 → R`. -/
 @[simps! symm_apply]
-def Quaternion.equivTuple (R : Type*) [One R] [Neg R] : ℍ[R] ≃ (Fin 4 → R) :=
-  QuaternionAlgebra.equivTuple _ _
+def Quaternion.equivTuple (R : Type*) [Zero R] [One R] [Neg R] : ℍ[R] ≃ (Fin 4 → R) :=
+  QuaternionAlgebra.equivTuple _ _ _
 
 @[simp]
-theorem Quaternion.equivTuple_apply (R : Type*) [One R] [Neg R] (x : ℍ[R]) :
+theorem Quaternion.equivTuple_apply (R : Type*) [Zero R] [One R] [Neg R] (x : ℍ[R]) :
     Quaternion.equivTuple R x = ![x.re, x.imI, x.imJ, x.imK] :=
   rfl
 
-instance {R : Type*} [One R] [Neg R] [Subsingleton R] : Subsingleton ℍ[R] :=
-  inferInstanceAs (Subsingleton <| ℍ[R, -1, -1])
-instance {R : Type*} [One R] [Neg R] [Nontrivial R] : Nontrivial ℍ[R] :=
-  inferInstanceAs (Nontrivial <| ℍ[R, -1, -1])
+instance {R : Type*} [Zero R] [One R] [Neg R] [Subsingleton R] : Subsingleton ℍ[R] :=
+  inferInstanceAs (Subsingleton <| ℍ[R, -1, 0, -1])
+instance {R : Type*} [Zero R] [One R] [Neg R] [Nontrivial R] : Nontrivial ℍ[R] :=
+  inferInstanceAs (Nontrivial <| ℍ[R, -1, 0, -1])
 
 namespace Quaternion
 
@@ -754,23 +801,23 @@ instance : CoeTC R ℍ[R] := ⟨coe⟩
 
 instance instRing : Ring ℍ[R] := QuaternionAlgebra.instRing
 
-instance : Inhabited ℍ[R] := inferInstanceAs <| Inhabited ℍ[R,-1,-1]
+instance : Inhabited ℍ[R] := inferInstanceAs <| Inhabited ℍ[R,-1, 0, -1]
 
-instance [SMul S R] : SMul S ℍ[R] := inferInstanceAs <| SMul S ℍ[R,-1,-1]
+instance [SMul S R] : SMul S ℍ[R] := inferInstanceAs <| SMul S ℍ[R,-1, 0, -1]
 
 instance [SMul S T] [SMul S R] [SMul T R] [IsScalarTower S T R] : IsScalarTower S T ℍ[R] :=
-  inferInstanceAs <| IsScalarTower S T ℍ[R,-1,-1]
+  inferInstanceAs <| IsScalarTower S T ℍ[R,-1,0,-1]
 
 instance [SMul S R] [SMul T R] [SMulCommClass S T R] : SMulCommClass S T ℍ[R] :=
-  inferInstanceAs <| SMulCommClass S T ℍ[R,-1,-1]
+  inferInstanceAs <| SMulCommClass S T ℍ[R,-1,0,-1]
 
 protected instance algebra [CommSemiring S] [Algebra S R] : Algebra S ℍ[R] :=
-  inferInstanceAs <| Algebra S ℍ[R,-1,-1]
+  inferInstanceAs <| Algebra S ℍ[R,-1,0,-1]
 
 -- Porting note: added shortcut
 instance : Star ℍ[R] := QuaternionAlgebra.instStarQuaternionAlgebra
 instance : StarRing ℍ[R] := QuaternionAlgebra.instStarRing
-instance : IsStarNormal a := inferInstanceAs <| IsStarNormal (R := ℍ[R,-1,-1]) a
+instance : IsStarNormal a := inferInstanceAs <| IsStarNormal (R := ℍ[R,-1,0,-1]) a
 
 @[ext]
 theorem ext : a.re = b.re → a.imI = b.imI → a.imJ = b.imJ → a.imK = b.imK → a = b :=
@@ -880,19 +927,19 @@ theorem coe_sub : ((x - y : R) : ℍ[R]) = x - y :=
 
 @[simp]
 theorem mul_re : (a * b).re = a.re * b.re - a.imI * b.imI - a.imJ * b.imJ - a.imK * b.imK :=
-  (QuaternionAlgebra.mul_re a b).trans <| by simp only [one_mul, neg_mul, sub_eq_add_neg, neg_neg]
+  (QuaternionAlgebra.mul_re a b).trans <| by simp [one_mul, neg_mul, sub_eq_add_neg, neg_neg]
 
 @[simp]
 theorem mul_imI : (a * b).imI = a.re * b.imI + a.imI * b.re + a.imJ * b.imK - a.imK * b.imJ :=
-  (QuaternionAlgebra.mul_imI a b).trans <| by simp only [one_mul, neg_mul, sub_eq_add_neg, neg_neg]
+  (QuaternionAlgebra.mul_imI a b).trans <| by ring
 
 @[simp]
 theorem mul_imJ : (a * b).imJ = a.re * b.imJ - a.imI * b.imK + a.imJ * b.re + a.imK * b.imI :=
-  (QuaternionAlgebra.mul_imJ a b).trans <| by simp only [one_mul, neg_mul, sub_eq_add_neg, neg_neg]
+  (QuaternionAlgebra.mul_imJ a b).trans <| by ring
 
 @[simp]
 theorem mul_imK : (a * b).imK = a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re :=
-  (QuaternionAlgebra.mul_imK a b).trans <| by simp only [one_mul, neg_mul, sub_eq_add_neg, neg_neg]
+  (QuaternionAlgebra.mul_imK a b).trans <| by ring
 
 @[simp, norm_cast]
 theorem coe_mul : ((x * y : R) : ℍ[R]) = x * y := QuaternionAlgebra.coe_mul x y
@@ -1020,16 +1067,17 @@ theorem algebraMap_injective : (algebraMap R ℍ[R] : _ → _).Injective :=
 theorem smul_coe : x • (y : ℍ[R]) = ↑(x * y) :=
   QuaternionAlgebra.smul_coe x y
 
-instance : Module.Finite R ℍ[R] := inferInstanceAs <| Module.Finite R ℍ[R,-1,-1]
-instance : Module.Free R ℍ[R] := inferInstanceAs <| Module.Free R ℍ[R,-1,-1]
+instance : Module.Finite R ℍ[R] := inferInstanceAs <| Module.Finite R ℍ[R,-1,0,-1]
+instance : Module.Free R ℍ[R] := inferInstanceAs <| Module.Free R ℍ[R,-1,0,-1]
 
 theorem rank_eq_four [StrongRankCondition R] : Module.rank R ℍ[R] = 4 :=
-  QuaternionAlgebra.rank_eq_four _ _
+  QuaternionAlgebra.rank_eq_four _ _ _
 
 theorem finrank_eq_four [StrongRankCondition R] : Module.finrank R ℍ[R] = 4 :=
-  QuaternionAlgebra.finrank_eq_four _ _
+  QuaternionAlgebra.finrank_eq_four _ _ _
 
-@[simp] theorem star_re : (star a).re = a.re := rfl
+@[simp] theorem star_re : (star a).re = a.re := by
+  rw [QuaternionAlgebra.re_star, zero_mul, add_zero]
 
 @[simp] theorem star_imI : (star a).imI = -a.imI := rfl
 
@@ -1039,33 +1087,31 @@ theorem finrank_eq_four [StrongRankCondition R] : Module.finrank R ℍ[R] = 4 :=
 
 @[simp] theorem star_im : (star a).im = -a.im := a.im_star
 
-nonrec theorem self_add_star' : a + star a = ↑(2 * a.re) :=
-  a.self_add_star'
+nonrec theorem self_add_star' : a + star a = ↑(2 * a.re) := by
+  simp [a.self_add_star', Quaternion.coe]
 
-nonrec theorem self_add_star : a + star a = 2 * a.re :=
-  a.self_add_star
+nonrec theorem self_add_star : a + star a = 2 * a.re := by
+  simp [a.self_add_star, Quaternion.coe]
 
-nonrec theorem star_add_self' : star a + a = ↑(2 * a.re) :=
-  a.star_add_self'
+nonrec theorem star_add_self' : star a + a = ↑(2 * a.re) := by
+  simp [a.star_add_self', Quaternion.coe]
 
-nonrec theorem star_add_self : star a + a = 2 * a.re :=
-  a.star_add_self
+nonrec theorem star_add_self : star a + a = 2 * a.re := by
+  simp [a.star_add_self, Quaternion.coe]
 
-nonrec theorem star_eq_two_re_sub : star a = ↑(2 * a.re) - a :=
-  a.star_eq_two_re_sub
+nonrec theorem star_eq_two_re_sub : star a = ↑(2 * a.re) - a := by
+  simp [a.star_eq_two_re_sub, Quaternion.coe]
 
 @[simp, norm_cast]
 theorem star_coe : star (x : ℍ[R]) = x :=
   QuaternionAlgebra.star_coe x
 
 @[simp]
-theorem im_star : star a.im = -a.im :=
-  QuaternionAlgebra.im_star _
+theorem im_star : star a.im = -a.im := by ext <;> simp
 
 @[simp]
 theorem star_smul [Monoid S] [DistribMulAction S R] (s : S) (a : ℍ[R]) :
-    star (s • a) = s • star a :=
-  QuaternionAlgebra.star_smul _ _
+    star (s • a) = s • star a := QuaternionAlgebra.star_smul' s a
 
 theorem eq_re_of_eq_coe {a : ℍ[R]} {x : R} (h : a = x) : a = a.re :=
   QuaternionAlgebra.eq_re_of_eq_coe h
@@ -1308,34 +1354,34 @@ open Quaternion
 
 section QuaternionAlgebra
 
-variable {R : Type*} (c₁ c₂ : R)
+variable {R : Type*} (c₁ c₂ c₃ : R)
 
 private theorem pow_four [Infinite R] : #R ^ 4 = #R :=
   power_nat_eq (aleph0_le_mk R) <| by decide
 
 /-- The cardinality of a quaternion algebra, as a type. -/
-theorem mk_quaternionAlgebra : #(ℍ[R,c₁,c₂]) = #R ^ 4 := by
-  rw [mk_congr (QuaternionAlgebra.equivProd c₁ c₂)]
+theorem mk_quaternionAlgebra : #(ℍ[R,c₁,c₂,c₃]) = #R ^ 4 := by
+  rw [mk_congr (QuaternionAlgebra.equivProd c₁ c₂ c₃)]
   simp only [mk_prod, lift_id]
   ring
 
 @[simp]
-theorem mk_quaternionAlgebra_of_infinite [Infinite R] : #(ℍ[R,c₁,c₂]) = #R := by
+theorem mk_quaternionAlgebra_of_infinite [Infinite R] : #(ℍ[R,c₁,c₂,c₃]) = #R := by
   rw [mk_quaternionAlgebra, pow_four]
 
 /-- The cardinality of a quaternion algebra, as a set. -/
-theorem mk_univ_quaternionAlgebra : #(Set.univ : Set ℍ[R,c₁,c₂]) = #R ^ 4 := by
+theorem mk_univ_quaternionAlgebra : #(Set.univ : Set ℍ[R,c₁,c₂,c₃]) = #R ^ 4 := by
   rw [mk_univ, mk_quaternionAlgebra]
 
 theorem mk_univ_quaternionAlgebra_of_infinite [Infinite R] :
-    #(Set.univ : Set ℍ[R,c₁,c₂]) = #R := by rw [mk_univ_quaternionAlgebra, pow_four]
+    #(Set.univ : Set ℍ[R,c₁,c₂,c₃]) = #R := by rw [mk_univ_quaternionAlgebra, pow_four]
 
 /-- Show the quaternion ⟨w, x, y, z⟩ as a string "{ re := w, imI := x, imJ := y, imK := z }".
 
 For the typical case of quaternions over ℝ, each component will show as a Cauchy sequence due to
 the way Real numbers are represented.
 -/
-instance [Repr R] {a b : R} : Repr ℍ[R, a, b] where
+instance [Repr R] {a b c : R} : Repr ℍ[R, a, b, c] where
   reprPrec q _ :=
     s!"\{ re := {repr q.re}, imI := {repr q.imI}, imJ := {repr q.imJ}, imK := {repr q.imK} }"
 
@@ -1343,22 +1389,22 @@ end QuaternionAlgebra
 
 section Quaternion
 
-variable (R : Type*) [One R] [Neg R]
+variable (R : Type*) [Zero R] [One R] [Neg R]
 
 /-- The cardinality of the quaternions, as a type. -/
 @[simp]
 theorem mk_quaternion : #(ℍ[R]) = #R ^ 4 :=
-  mk_quaternionAlgebra _ _
+  mk_quaternionAlgebra _ _ _
 
 theorem mk_quaternion_of_infinite [Infinite R] : #(ℍ[R]) = #R :=
-  mk_quaternionAlgebra_of_infinite _ _
+  mk_quaternionAlgebra_of_infinite _ _ _
 
 /-- The cardinality of the quaternions, as a set. -/
 theorem mk_univ_quaternion : #(Set.univ : Set ℍ[R]) = #R ^ 4 :=
-  mk_univ_quaternionAlgebra _ _
+  mk_univ_quaternionAlgebra _ _ _
 
 theorem mk_univ_quaternion_of_infinite [Infinite R] : #(Set.univ : Set ℍ[R]) = #R :=
-  mk_univ_quaternionAlgebra_of_infinite _ _
+  mk_univ_quaternionAlgebra_of_infinite _ _ _
 
 end Quaternion
 
diff --git a/Mathlib/Algebra/QuaternionBasis.lean b/Mathlib/Algebra/QuaternionBasis.lean
index 0bbcb83c8be73..9fcaf7da1c225 100644
--- a/Mathlib/Algebra/QuaternionBasis.lean
+++ b/Mathlib/Algebra/QuaternionBasis.lean
@@ -11,11 +11,11 @@ import Mathlib.Tactic.Ring
 
 ## Main definitions
 
-* `QuaternionAlgebra.Basis A c₁ c₂`: a basis for a subspace of an `R`-algebra `A` that has the
-  same algebra structure as `ℍ[R,c₁,c₂]`.
-* `QuaternionAlgebra.Basis.self R`: the canonical basis for `ℍ[R,c₁,c₂]`.
+* `QuaternionAlgebra.Basis A c₁ c₂ c₃`: a basis for a subspace of an `R`-algebra `A` that has the
+  same algebra structure as `ℍ[R,c₁,c₂,c₃]`.
+* `QuaternionAlgebra.Basis.self R`: the canonical basis for `ℍ[R,c₁,c₂,c₃]`.
 * `QuaternionAlgebra.Basis.compHom b f`: transform a basis `b` by an AlgHom `f`.
-* `QuaternionAlgebra.lift`: Define an `AlgHom` out of `ℍ[R,c₁,c₂]` by its action on the basis
+* `QuaternionAlgebra.lift`: Define an `AlgHom` out of `ℍ[R,c₁,c₂,c₃]` by its action on the basis
   elements `i`, `j`, and `k`. In essence, this is a universal property. Analogous to `Complex.lift`,
   but takes a bundled `QuaternionAlgebra.Basis` instead of just a `Subtype` as the amount of
   data / proves is non-negligible.
@@ -27,26 +27,27 @@ open Quaternion
 namespace QuaternionAlgebra
 
 /-- A quaternion basis contains the information both sufficient and necessary to construct an
-`R`-algebra homomorphism from `ℍ[R,c₁,c₂]` to `A`; or equivalently, a surjective
-`R`-algebra homomorphism from `ℍ[R,c₁,c₂]` to an `R`-subalgebra of `A`.
+`R`-algebra homomorphism from `ℍ[R,c₁,c₂,c₃]` to `A`; or equivalently, a surjective
+`R`-algebra homomorphism from `ℍ[R,c₁,c₂,c₃]` to an `R`-subalgebra of `A`.
 
 Note that for definitional convenience, `k` is provided as a field even though `i_mul_j` fully
 determines it. -/
-structure Basis {R : Type*} (A : Type*) [CommRing R] [Ring A] [Algebra R A] (c₁ c₂ : R) where
+structure Basis {R : Type*} (A : Type*) [CommRing R] [Ring A] [Algebra R A] (c₁ c₂ c₃ : R) where
   (i j k : A)
-  i_mul_i : i * i = c₁ • (1 : A)
-  j_mul_j : j * j = c₂ • (1 : A)
+  i_mul_i : i * i = c₁ • (1 : A) + c₂ • i
+  j_mul_j : j * j = c₃ • (1 : A)
   i_mul_j : i * j = k
-  j_mul_i : j * i = -k
+  j_mul_i : j * i = c₂ • j - k
 
 variable {R : Type*} {A B : Type*} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B]
-variable {c₁ c₂ : R}
+variable {c₁ c₂ c₃: R}
 
 namespace Basis
 
 /-- Since `k` is redundant, it is not necessary to show `q₁.k = q₂.k` when showing `q₁ = q₂`. -/
 @[ext]
-protected theorem ext ⦃q₁ q₂ : Basis A c₁ c₂⦄ (hi : q₁.i = q₂.i) (hj : q₁.j = q₂.j) : q₁ = q₂ := by
+protected theorem ext ⦃q₁ q₂ : Basis A c₁ c₂ c₃⦄ (hi : q₁.i = q₂.i)
+    (hj : q₁.j = q₂.j) : q₁ = q₂ := by
   cases q₁; rename_i q₁_i_mul_j _
   cases q₂; rename_i q₂_i_mul_j _
   congr
@@ -57,7 +58,7 @@ variable (R)
 
 /-- There is a natural quaternionic basis for the `QuaternionAlgebra`. -/
 @[simps i j k]
-protected def self : Basis ℍ[R,c₁,c₂] c₁ c₂ where
+protected def self : Basis ℍ[R,c₁,c₂,c₃] c₁ c₂ c₃ where
   i := ⟨0, 1, 0, 0⟩
   i_mul_i := by ext <;> simp
   j := ⟨0, 0, 1, 0⟩
@@ -68,64 +69,70 @@ protected def self : Basis ℍ[R,c₁,c₂] c₁ c₂ where
 
 variable {R}
 
-instance : Inhabited (Basis ℍ[R,c₁,c₂] c₁ c₂) :=
+instance : Inhabited (Basis ℍ[R,c₁,c₂,c₃] c₁ c₂ c₃) :=
   ⟨Basis.self R⟩
 
-variable (q : Basis A c₁ c₂)
+variable (q : Basis A c₁ c₂ c₃)
 
 attribute [simp] i_mul_i j_mul_j i_mul_j j_mul_i
 
 @[simp]
-theorem i_mul_k : q.i * q.k = c₁ • q.j := by
-  rw [← i_mul_j, ← mul_assoc, i_mul_i, smul_mul_assoc, one_mul]
+theorem i_mul_k : q.i * q.k = c₁ • q.j + c₂ • q.k := by
+  rw [← i_mul_j, ← mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, smul_mul_assoc]
 
 @[simp]
 theorem k_mul_i : q.k * q.i = -c₁ • q.j := by
-  rw [← i_mul_j, mul_assoc, j_mul_i, mul_neg, i_mul_k, neg_smul]
+  rw [← i_mul_j, mul_assoc, j_mul_i, mul_sub, i_mul_k, neg_smul, mul_smul_comm, i_mul_j]
+  linear_combination (norm := module)
 
 @[simp]
-theorem k_mul_j : q.k * q.j = c₂ • q.i := by
+theorem k_mul_j : q.k * q.j = c₃ • q.i := by
   rw [← i_mul_j, mul_assoc, j_mul_j, mul_smul_comm, mul_one]
 
 @[simp]
-theorem j_mul_k : q.j * q.k = -c₂ • q.i := by
-  rw [← i_mul_j, ← mul_assoc, j_mul_i, neg_mul, k_mul_j, neg_smul]
+theorem j_mul_k : q.j * q.k = (c₂ * c₃) • 1 - c₃ • q.i := by
+  rw [← i_mul_j, ← mul_assoc, j_mul_i, sub_mul, smul_mul_assoc, j_mul_j, ← smul_assoc, k_mul_j]
+  rfl
 
 @[simp]
-theorem k_mul_k : q.k * q.k = -((c₁ * c₂) • (1 : A)) := by
-  rw [← i_mul_j, mul_assoc, ← mul_assoc q.j _ _, j_mul_i, ← i_mul_j, ← mul_assoc, mul_neg, ←
-    mul_assoc, i_mul_i, smul_mul_assoc, one_mul, neg_mul, smul_mul_assoc, j_mul_j, smul_smul]
+theorem k_mul_k : q.k * q.k = -((c₁ * c₃) • (1 : A)) := by
+  rw [← i_mul_j, mul_assoc, ← mul_assoc q.j _ _, j_mul_i, ← i_mul_j, ← mul_assoc, mul_sub, ←
+    mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, sub_mul, smul_mul_assoc, mul_smul_comm,
+    smul_mul_assoc, mul_assoc, j_mul_j, add_mul, smul_mul_assoc, j_mul_j, smul_smul,
+    smul_mul_assoc, mul_assoc, j_mul_j]
+  linear_combination (norm := module)
+
 
 /-- Intermediate result used to define `QuaternionAlgebra.Basis.liftHom`. -/
-def lift (x : ℍ[R,c₁,c₂]) : A :=
+def lift (x : ℍ[R,c₁,c₂,c₃]) : A :=
   algebraMap R _ x.re + x.imI • q.i + x.imJ • q.j + x.imK • q.k
 
-theorem lift_zero : q.lift (0 : ℍ[R,c₁,c₂]) = 0 := by simp [lift]
+theorem lift_zero : q.lift (0 : ℍ[R,c₁,c₂,c₃]) = 0 := by simp [lift]
 
-theorem lift_one : q.lift (1 : ℍ[R,c₁,c₂]) = 1 := by simp [lift]
+theorem lift_one : q.lift (1 : ℍ[R,c₁,c₂,c₃]) = 1 := by simp [lift]
 
-theorem lift_add (x y : ℍ[R,c₁,c₂]) : q.lift (x + y) = q.lift x + q.lift y := by
+theorem lift_add (x y : ℍ[R,c₁,c₂,c₃]) : q.lift (x + y) = q.lift x + q.lift y := by
   simp only [lift, add_re, map_add, add_imI, add_smul, add_imJ, add_imK]
   abel
 
-theorem lift_mul (x y : ℍ[R,c₁,c₂]) : q.lift (x * y) = q.lift x * q.lift y := by
+theorem lift_mul (x y : ℍ[R,c₁,c₂,c₃]) : q.lift (x * y) = q.lift x * q.lift y := by
   simp only [lift, Algebra.algebraMap_eq_smul_one]
   simp_rw [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one, smul_smul]
   simp only [i_mul_i, j_mul_j, i_mul_j, j_mul_i, i_mul_k, k_mul_i, k_mul_j, j_mul_k, k_mul_k]
   simp only [smul_smul, smul_neg, sub_eq_add_neg, add_smul, ← add_assoc, mul_neg, neg_smul]
-  simp only [mul_right_comm _ _ (c₁ * c₂), mul_comm _ (c₁ * c₂)]
+  simp only [mul_right_comm _ _ (c₁ * c₃), mul_comm _ (c₁ * c₃)]
   simp only [mul_comm _ c₁, mul_right_comm _ _ c₁]
-  simp only [mul_comm _ c₂, mul_right_comm _ _ c₂]
+  simp only [mul_comm _ c₂, mul_right_comm _ _ c₃]
   simp only [← mul_comm c₁ c₂, ← mul_assoc]
   simp only [mul_re, sub_eq_add_neg, add_smul, neg_smul, mul_imI, ← add_assoc, mul_imJ, mul_imK]
-  abel
+  linear_combination (norm := module)
 
-theorem lift_smul (r : R) (x : ℍ[R,c₁,c₂]) : q.lift (r • x) = r • q.lift x := by
+theorem lift_smul (r : R) (x : ℍ[R,c₁,c₂,c₃]) : q.lift (r • x) = r • q.lift x := by
   simp [lift, mul_smul, ← Algebra.smul_def]
 
 /-- A `QuaternionAlgebra.Basis` implies an `AlgHom` from the quaternions. -/
 @[simps!]
-def liftHom : ℍ[R,c₁,c₂] →ₐ[R] A :=
+def liftHom : ℍ[R,c₁,c₂,c₃] →ₐ[R] A :=
   AlgHom.mk'
     { toFun := q.lift
       map_zero' := q.lift_zero
@@ -135,20 +142,20 @@ def liftHom : ℍ[R,c₁,c₂] →ₐ[R] A :=
 
 /-- Transform a `QuaternionAlgebra.Basis` through an `AlgHom`. -/
 @[simps i j k]
-def compHom (F : A →ₐ[R] B) : Basis B c₁ c₂ where
+def compHom (F : A →ₐ[R] B) : Basis B c₁ c₂ c₃ where
   i := F q.i
-  i_mul_i := by rw [← map_mul, q.i_mul_i, map_smul, map_one]
+  i_mul_i := by rw [← map_mul, q.i_mul_i, map_add, map_smul, map_smul, map_one]
   j := F q.j
   j_mul_j := by rw [← map_mul, q.j_mul_j, map_smul, map_one]
   k := F q.k
   i_mul_j := by rw [← map_mul, q.i_mul_j]
-  j_mul_i := by rw [← map_mul, q.j_mul_i, map_neg]
+  j_mul_i := by rw [← map_mul, q.j_mul_i, map_sub, map_smul]
 
 end Basis
 
 /-- A quaternionic basis on `A` is equivalent to a map from the quaternion algebra to `A`. -/
 @[simps]
-def lift : Basis A c₁ c₂ ≃ (ℍ[R,c₁,c₂] →ₐ[R] A) where
+def lift : Basis A c₁ c₂ c₃ ≃ (ℍ[R,c₁,c₂,c₃] →ₐ[R] A) where
   toFun := Basis.liftHom
   invFun := (Basis.self R).compHom
   left_inv q := by ext <;> simp [Basis.lift]
@@ -162,7 +169,7 @@ def lift : Basis A c₁ c₂ ≃ (ℍ[R,c₁,c₂] →ₐ[R] A) where
 
 /-- Two `R`-algebra morphisms from a quaternion algebra are equal if they agree on `i` and `j`. -/
 @[ext]
-theorem hom_ext ⦃f g : ℍ[R,c₁,c₂] →ₐ[R] A⦄
+theorem hom_ext ⦃f g : ℍ[R,c₁,c₂,c₃] →ₐ[R] A⦄
     (hi : f (Basis.self R).i = g (Basis.self R).i) (hj : f (Basis.self R).j = g (Basis.self R).j) :
     f = g :=
   lift.symm.injective <| Basis.ext hi hj
diff --git a/Mathlib/Analysis/Quaternion.lean b/Mathlib/Analysis/Quaternion.lean
index 9f75be8137503..6c28375ee66a8 100644
--- a/Mathlib/Analysis/Quaternion.lean
+++ b/Mathlib/Analysis/Quaternion.lean
@@ -163,7 +163,7 @@ theorem norm_piLp_equiv_symm_equivTuple (x : ℍ) :
 /-- `QuaternionAlgebra.linearEquivTuple` as a `LinearIsometryEquiv`. -/
 @[simps apply symm_apply]
 noncomputable def linearIsometryEquivTuple : ℍ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 4) :=
-  { (QuaternionAlgebra.linearEquivTuple (-1 : ℝ) (-1 : ℝ)).trans
+  { (QuaternionAlgebra.linearEquivTuple (-1 : ℝ) (0 : ℝ) (-1 : ℝ)).trans
       (WithLp.linearEquiv 2 ℝ (Fin 4 → ℝ)).symm with
     toFun := fun a => !₂[a.1, a.2, a.3, a.4]
     invFun := fun a => ⟨a 0, a 1, a 2, a 3⟩
@@ -209,13 +209,16 @@ variable {α : Type*}
 
 @[simp, norm_cast]
 theorem hasSum_coe {f : α → ℝ} {r : ℝ} : HasSum (fun a => (f a : ℍ)) (↑r : ℍ) ↔ HasSum f r :=
-  ⟨fun h => by simpa only using h.map (show ℍ →ₗ[ℝ] ℝ from QuaternionAlgebra.reₗ _ _) continuous_re,
+  ⟨fun h => by
+    simpa only using
+    h.map (show ℍ →ₗ[ℝ] ℝ from QuaternionAlgebra.reₗ _ _ _) continuous_re,
     fun h => by simpa only using h.map (algebraMap ℝ ℍ) (continuous_algebraMap _ _)⟩
 
 @[simp, norm_cast]
 theorem summable_coe {f : α → ℝ} : (Summable fun a => (f a : ℍ)) ↔ Summable f := by
   simpa only using
-    Summable.map_iff_of_leftInverse (algebraMap ℝ ℍ) (show ℍ →ₗ[ℝ] ℝ from QuaternionAlgebra.reₗ _ _)
+    Summable.map_iff_of_leftInverse (algebraMap ℝ ℍ) (show ℍ →ₗ[ℝ] ℝ from
+      QuaternionAlgebra.reₗ _ _ _)
       (continuous_algebraMap _ _) continuous_re coe_re
 
 @[norm_cast]
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
index 9abbbe4782efb..22f87694b197f 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
@@ -242,7 +242,7 @@ theorem Q_apply (v : R × R) : Q c₁ c₂ v = c₁ * (v.1 * v.1) + c₂ * (v.2
 
 /-- The quaternion basis vectors within the algebra. -/
 @[simps i j k]
-def quaternionBasis : QuaternionAlgebra.Basis (CliffordAlgebra (Q c₁ c₂)) c₁ c₂ where
+def quaternionBasis : QuaternionAlgebra.Basis (CliffordAlgebra (Q c₁ c₂)) c₁ 0 c₂ where
   i := ι (Q c₁ c₂) (1, 0)
   j := ι (Q c₁ c₂) (0, 1)
   k := ι (Q c₁ c₂) (1, 0) * ι (Q c₁ c₂) (0, 1)
@@ -254,16 +254,16 @@ def quaternionBasis : QuaternionAlgebra.Basis (CliffordAlgebra (Q c₁ c₂)) c
     simp
   i_mul_j := rfl
   j_mul_i := by
-    rw [eq_neg_iff_add_eq_zero, ι_mul_ι_add_swap, QuadraticMap.polar]
+    rw [zero_smul, zero_sub, eq_neg_iff_add_eq_zero, ι_mul_ι_add_swap, QuadraticMap.polar]
     simp
 
 variable {c₁ c₂}
 
 /-- Intermediate result of `CliffordAlgebraQuaternion.equiv`: clifford algebras over
 `CliffordAlgebraQuaternion.Q` can be converted to `ℍ[R,c₁,c₂]`. -/
-def toQuaternion : CliffordAlgebra (Q c₁ c₂) →ₐ[R] ℍ[R,c₁,c₂] :=
+def toQuaternion : CliffordAlgebra (Q c₁ c₂) →ₐ[R] ℍ[R,c₁,0,c₂] :=
   CliffordAlgebra.lift (Q c₁ c₂)
-    ⟨{  toFun := fun v => (⟨0, v.1, v.2, 0⟩ : ℍ[R,c₁,c₂])
+    ⟨{  toFun := fun v => (⟨0, v.1, v.2, 0⟩ : ℍ[R,c₁,0,c₂])
         map_add' := fun v₁ v₂ => by simp
         map_smul' := fun r v => by dsimp; rw [mul_zero] }, fun v => by
       dsimp
@@ -272,7 +272,7 @@ def toQuaternion : CliffordAlgebra (Q c₁ c₂) →ₐ[R] ℍ[R,c₁,c₂] :=
 
 @[simp]
 theorem toQuaternion_ι (v : R × R) :
-    toQuaternion (ι (Q c₁ c₂) v) = (⟨0, v.1, v.2, 0⟩ : ℍ[R,c₁,c₂]) :=
+    toQuaternion (ι (Q c₁ c₂) v) = (⟨0, v.1, v.2, 0⟩ : ℍ[R,c₁,0,c₂]) :=
   CliffordAlgebra.lift_ι_apply _ _ v
 
 /-- The "clifford conjugate" maps to the quaternion conjugate. -/
@@ -280,22 +280,18 @@ theorem toQuaternion_star (c : CliffordAlgebra (Q c₁ c₂)) :
     toQuaternion (star c) = star (toQuaternion c) := by
   simp only [CliffordAlgebra.star_def']
   induction c using CliffordAlgebra.induction with
-  | algebraMap r =>
-    simp only [reverse.commutes, AlgHom.commutes, QuaternionAlgebra.coe_algebraMap,
-      QuaternionAlgebra.star_coe]
-  | ι x =>
-    rw [reverse_ι, involute_ι, toQuaternion_ι, map_neg, toQuaternion_ι,
-      QuaternionAlgebra.neg_mk, star_mk, neg_zero]
-  | mul x₁ x₂ hx₁ hx₂ => simp only [reverse.map_mul, map_mul, hx₁, hx₂, star_mul]
-  | add x₁ x₂ hx₁ hx₂ => simp only [reverse.map_add, map_add, hx₁, hx₂, star_add]
+  | algebraMap r => simp
+  | ι x => simp
+  | mul x₁ x₂ hx₁ hx₂ => simp [hx₁, hx₂]
+  | add x₁ x₂ hx₁ hx₂ => simp [hx₁, hx₂]
 
 /-- Map a quaternion into the clifford algebra. -/
-def ofQuaternion : ℍ[R,c₁,c₂] →ₐ[R] CliffordAlgebra (Q c₁ c₂) :=
+def ofQuaternion : ℍ[R,c₁,0,c₂] →ₐ[R] CliffordAlgebra (Q c₁ c₂) :=
   (quaternionBasis c₁ c₂).liftHom
 
 @[simp]
 theorem ofQuaternion_mk (a₁ a₂ a₃ a₄ : R) :
-    ofQuaternion (⟨a₁, a₂, a₃, a₄⟩ : ℍ[R,c₁,c₂]) =
+    ofQuaternion (⟨a₁, a₂, a₃, a₄⟩ : ℍ[R,c₁,0,c₂]) =
       algebraMap R _ a₁ + a₂ • ι (Q c₁ c₂) (1, 0) + a₃ • ι (Q c₁ c₂) (0, 1) +
         a₄ • (ι (Q c₁ c₂) (1, 0) * ι (Q c₁ c₂) (0, 1)) :=
   rfl
@@ -319,23 +315,23 @@ theorem ofQuaternion_toQuaternion (c : CliffordAlgebra (Q c₁ c₂)) :
 
 @[simp]
 theorem toQuaternion_comp_ofQuaternion :
-    toQuaternion.comp ofQuaternion = AlgHom.id R ℍ[R,c₁,c₂] := by
+    toQuaternion.comp ofQuaternion = AlgHom.id R ℍ[R,c₁,0,c₂] := by
   ext : 1 <;> simp
 
 @[simp]
-theorem toQuaternion_ofQuaternion (q : ℍ[R,c₁,c₂]) : toQuaternion (ofQuaternion q) = q :=
+theorem toQuaternion_ofQuaternion (q : ℍ[R,c₁,0,c₂]) : toQuaternion (ofQuaternion q) = q :=
   AlgHom.congr_fun toQuaternion_comp_ofQuaternion q
 
 /-- The clifford algebra over `CliffordAlgebraQuaternion.Q c₁ c₂` is isomorphic as an `R`-algebra
 to `ℍ[R,c₁,c₂]`. -/
 @[simps!]
-protected def equiv : CliffordAlgebra (Q c₁ c₂) ≃ₐ[R] ℍ[R,c₁,c₂] :=
+protected def equiv : CliffordAlgebra (Q c₁ c₂) ≃ₐ[R] ℍ[R,c₁,0,c₂] :=
   AlgEquiv.ofAlgHom toQuaternion ofQuaternion toQuaternion_comp_ofQuaternion
     ofQuaternion_comp_toQuaternion
 
 /-- The quaternion conjugate maps to the "clifford conjugate" (aka `star`). -/
 @[simp]
-theorem ofQuaternion_star (q : ℍ[R,c₁,c₂]) : ofQuaternion (star q) = star (ofQuaternion q) :=
+theorem ofQuaternion_star (q : ℍ[R,c₁,0,c₂]) : ofQuaternion (star q) = star (ofQuaternion q) :=
   CliffordAlgebraQuaternion.equiv.injective <| by
     rw [equiv_apply, equiv_apply, toQuaternion_star, toQuaternion_ofQuaternion,
       toQuaternion_ofQuaternion]