# Zulip Chat Archive

## Stream: maths

### Topic: Quadratic fields

#### 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