Arithmetic of quadratic fields

[riccardobrasca]

trafficstars

Basic arithmetic of quadratic fields (ring of integers, discriminant and so on) should now not be too difficult.

https://en.wikipedia.org/wiki/Quadratic_field https://en.wikipedia.org/wiki/Quadratic_integer

[Vierkantor]

This is very much in my area of interest, although I got a bit sidetracked with more computer sciency issues at the moment... I might have some half-finished outdated files for you if you want to try and fix them up.

[riccardobrasca]

I am not going to work on this, I am already busy enough with flt-regular. But mathlib will soon know about the ring of integers of cyclotomic fields, so it is a little strange it doesn't know anything about quadratic fields.

In any case anyone interested should check here to see what we have already proved but not yet PRed.

[jcommelin]

Note that the number rings zsqrtd have been defined. So that's a start.

[kbuzzard]

Yeah but (as you know) some of these things aren't rings of integers, and some rings of integers aren't of this form. Maybe one way to proceed would be to define an "abstract Z[(1+sqrt(d))/2]" for d an integer congruent to 1 mod 4, like we have an "abstract Z[sqrt(d)]". I have a student working on Pell's equation by the way.

[jcommelin]

I'm not sure I follow what you mean with an "abstract foobar". I would imagine that we can just add instances saying that zsqrtd is a ring of integers under the suitable fact assumptions. And then add zsqrtdhalf (or whatever it should be called) as well.

Or is that what you meant?

[alreadydone]

New development at https://github.com/lean-forward/class-group-and-mordell-equation/blob/main/src/number_theory/quad_ring/basic.lean