feat: add Repr instance for quaternions (#13940)

Adds a Repr instance for QuaternionAlgebra. A quaternion <w, x, y, z> is shown as "{ re := w, imI := x, imJ := y, imK := z }". The components are displayed as Cauchy sequences for quaternions over the Reals.

Mathlib/Algebra/Quaternion.lean

@@ -1557,6 +1557,15 @@ theorem mk_univ_quaternionAlgebra_of_infinite [Infinite R] :
     #(Set.univ : Set ℍ[R,c₁,c₂]) = #R := by rw [mk_univ_quaternionAlgebra, pow_four]
 #align cardinal.mk_univ_quaternion_algebra_of_infinite Cardinal.mk_univ_quaternionAlgebra_of_infinite
 
+/-- 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
+  reprPrec q _ :=
+    s!"\{ re := {repr q.re}, imI := {repr q.imI}, imJ := {repr q.imJ}, imK := {repr q.imK} }"
+
 end QuaternionAlgebra
 
 section Quaternion

test/Quaternion.lean

@@ -0,0 +1,40 @@
+import Mathlib.Algebra.Quaternion
+import Mathlib.Data.Real.Basic
+import Mathlib.NumberTheory.Zsqrtd.GaussianInt
+
+open Quaternion
+/--
+info: { re := 0, imI := 0, imJ := 0, imK := 0 }
+-/
+#guard_msgs in
+#eval (0 : ℍ[ℚ])
+
+/--
+info: { re := 1, imI := 0, imJ := 0, imK := 0 }
+-/
+#guard_msgs in
+#eval (1 : ℍ[ℚ])
+
+/--
+info: { re := 4, imI := 0, imJ := 0, imK := 0 }
+-/
+#guard_msgs in
+#eval (4 : ℍ[ℚ])
+
+/--
+info: { re := Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/), imI := Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/), imJ := Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/), imK := Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/) }
+-/
+#guard_msgs in
+#eval (⟨0, 0, 0, 0⟩ : ℍ[ℝ])
+
+/--
+info: { re := Real.ofCauchy (sorry /- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, ... -/), imI := Real.ofCauchy (sorry /- 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, ... -/), imJ := Real.ofCauchy (sorry /- 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, ... -/), imK := Real.ofCauchy (sorry /- 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, ... -/) }
+-/
+#guard_msgs in
+#eval (⟨1, 2, 3, 4⟩ : ℍ[ℝ])
+
+/--
+info: { re := ⟨0, 0⟩, imI := ⟨0, 0⟩, imJ := ⟨0, 0⟩, imK := ⟨0, 0⟩ }
+-/
+#guard_msgs in
+#eval (0 : ℍ[GaussianInt])