From 8857292e0ebdf32509fb021df7bdeba56a455be1 Mon Sep 17 00:00:00 2001
From: pauldavidrowe <pauldavidrowe@gmail.com>
Date: Tue, 25 Jun 2024 22:19:55 +0000
Subject: [PATCH] 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 |  9 ++++++++
 test/Quaternion.lean            | 40 +++++++++++++++++++++++++++++++++
 2 files changed, 49 insertions(+)
 create mode 100644 test/Quaternion.lean

diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean
index 4d132cacf9ab1..9f4e14d5e4d60 100644
--- a/Mathlib/Algebra/Quaternion.lean
+++ b/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
diff --git a/test/Quaternion.lean b/test/Quaternion.lean
new file mode 100644
index 0000000000000..9fb39b008873b
--- /dev/null
+++ b/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])