feat(Algebra/QuaternionBasis): extensionality for algebra morphisms f…

…rom quaternions (#9441)

This result was basically already here, this just registers it with `ext`.

Mathlib/Algebra/QuaternionBasis.lean

@@ -180,4 +180,25 @@ def lift : Basis A c₁ c₂ ≃ (ℍ[R,c₁,c₂] →ₐ[R] A) where
     congr <;> simp
 #align quaternion_algebra.lift QuaternionAlgebra.lift
 
+/-- 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⦄
+    (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
+
 end QuaternionAlgebra
+
+namespace Quaternion
+variable {R A : Type*} [CommRing R] [Ring A] [Algebra R A]
+
+open QuaternionAlgebra (Basis)
+
+/-- Two `R`-algebra morphisms from the quaternions are equal if they agree on `i` and `j`. -/
+@[ext]
+theorem hom_ext ⦃f g : ℍ[R] →ₐ[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 :=
+  QuaternionAlgebra.hom_ext hi hj
+
+end Quaternion

Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean

@@ -357,8 +357,7 @@ theorem ofQuaternion_toQuaternion (c : CliffordAlgebra (Q c₁ c₂)) :
 @[simp]
 theorem toQuaternion_comp_ofQuaternion :
     toQuaternion.comp ofQuaternion = AlgHom.id R ℍ[R,c₁,c₂] := by
-  apply QuaternionAlgebra.lift.symm.injective
-  ext1 <;> dsimp [QuaternionAlgebra.Basis.lift] <;> simp
+  ext : 1 <;> simp
 #align clifford_algebra_quaternion.to_quaternion_comp_of_quaternion CliffordAlgebraQuaternion.toQuaternion_comp_ofQuaternion
 
 @[simp]