Repr instance for Quaternion

Stream: mathlib4

[Paul Rowe]

In another thread there was some discussion about a Repr instance for Quaternions. Two potentially reasonable options are

instance [Repr α] [One α] [Neg α] : Repr (Quaternion α) :=
  { reprPrec := fun q _ => s!"\{ re := {repr q.re}, imI := {repr q.imI}, imJ := {repr q.imJ}, imK := {repr q.imK} }" }

which mirrors the way a Quaternion is constructed as input.

Another suggestion was to mimic what was done for Complex

instance [Repr α] [One α] [Neg α] : Repr (Quaternion α) :=
  { reprPrec := fun q _ => s!"{repr q.re} + {repr q.imI}*I + {repr q.imJ}*J + {repr q.imK}*K" }

With this second option we would probably want to introduce a notation to match.

And of course there may be a better third option not yet considered. Any thoughts @Yury G. Kudryashov ?

[Yury G. Kudryashov]

I have no opinion. I have no plans to use quaternions in the near future.

[Eric Wieser]

My suggestion there was that we could have

def QuaternionAlgebra.I := { re := 0, im_i := 1, ... }

and then change the simp-normal forms everywhere

[Mr Proof]

My only suggestion is that would be best to have brackets around it, then it makes combining types easier. e.g. DualNumber (Quaternion Int). I don't think things are very consistent since GaussianInt is represented as ⟨ 3, 4⟩ but DualNumber Intis represented 3 + 4*ε. So probably doesn't really matter.

[Utensil Song]

It would be nice to have consistent and combinable reprs.

[Eric Wieser]

This is what the prec argument of reprPrec is for

[Eric Wieser]

The parentheses are only added when needed

[Eric Wieser]

Take a look at src#Complex.instRepr

[Paul Rowe]

I just created #13940 to add a Repr instance for quaternions. I chose the "{ re := w, imI := x, imJ := y, imK := z }" format, where each of w, x, y, z are formatted according to their type. In particular, if they are Reals, then the components display as Cauchy sequences.

This is my first PR so I'm quite happy to receive any suggestions for improvement.