## Stream: maths

#### Paul van Wamelen (Sep 04 2020 at 02:20):

I'd like to add the ring of quadratic integers for the case when d is 1 mod 4. So the ring of the integers adjoined with (1 + a square root of d)/2. What should these be called? We already have zsqrtd = ℤ√d. I was thinking of using 𝒪√d? What should the file be called? Also, the elements have the form a + b (1 + √d)/2 where a b : ℤ. Should I call a and b, re and im (as in zsqrtd)? I would rather just call them c1 and c2 (for component 1 and 2) especially since the components in the embedding in ℂ isn't the real and imaginary parts. I'd love to hear people's thoughts on this!

#### Kevin Buzzard (Sep 04 2020 at 08:07):

This is a very delicate question! Each new definition added to lean comes with a cost so you want to make sure you've got it right the first time. Are you happy to have these rings for d which aren't fundamental discriminants eg 45 or even 9?

#### Kevin Buzzard (Sep 04 2020 at 08:10):

Then there's the implementation question of whether you should define it under the hood to be a pair of integers (which Mario might be tempted to do) or as a quotient of Z[X] (which I'd be tempted to do). @Chris Hughes which one is the best idea?

#### Kevin Buzzard (Sep 04 2020 at 08:11):

This question doesn't matter to a mathematician because all we want is the interface, but someone has to make it and the job is very different depending on which definition you choose

#### Kevin Buzzard (Sep 04 2020 at 08:13):

I should say that your ideas all look fine to me and that you should perhaps allow all integers d in the definition and just make the ring structure for d congruent to 1 mod 4, but actually this then presents a problem for type class inference

#### Kevin Buzzard (Sep 04 2020 at 08:17):

Another approach would be to define integers of number fields, which I think we have already, and then define these functions c1 and c2 for the quadratic fields in question.

#### Kenny Lau (Sep 04 2020 at 08:34):

I propose defining Z[(1+sqrt(1+4k))/2]

#### Kenny Lau (Sep 04 2020 at 08:34):

just to make sure that it's always a ring

#### Kenny Lau (Sep 04 2020 at 08:59):

$\left(\frac{1+\sqrt{1+4k}}2\right)^2 = \frac{2+4k+2\sqrt{1+4k}}{4} = k + \frac{1+\sqrt{1+4k}}2$

#### Kenny Lau (Sep 04 2020 at 09:01):

you can call it Zhopsopft for "Z half one plus square-root one plus four times"

#### Chris Hughes (Sep 04 2020 at 09:12):

There is already zsqrtd. I agree with the simple construction as pairs, it will given some nicer definitional equalities.

#### Johan Commelin (Sep 05 2020 at 15:36):

We probably need a name for this gadget... should we have roi2 or quadratic_ring_of_integers that gives the correct thing for all non-square d?

#### Paul van Wamelen (Sep 05 2020 at 15:57):

I'm using d1_quadratic_int for now... (I think that is an improvement on Zhopsopft :grinning_face_with_smiling_eyes: )

#### Johan Commelin (Sep 05 2020 at 16:04):

@Kevin Buzzard would it make sense to define this to be int x int or int[epsilon] in the cases where Q[X](X^2 - d) is not a field?

#### Kevin Buzzard (Sep 05 2020 at 16:06):

Sure. I haven't looked but I bet that's what Mario did with Zsqrtd when d was a square. I was much less sure about how to deal with the d=1 mod 4 thing but maybe Kenny's solution is the best

Last updated: May 06 2021 at 17:38 UTC