Alex Meiburg

Stream: new members

[Alex Meiburg]

Hi! I'm brand new to Lean and just poking around in mathlib to see what's there. I see there's some algebraic number theory: definition of algebraic number fields, special stuff on Z[sqrt(d)] and Gaussian integers, and some class number stuff. But I couldn't find any actual "meat" of the theory, e.g. I couldn't even find a proof of what the integral closure of Z in Q[sqrt(d)] was. Is there somewhere and I'm missing it?

[Alex Meiburg]

If not, would that be a welcome thing to try and add? :) I'm sure it's written somewhere in some repository, but maybe to contribute it to mathlib in particular?

[Alex Meiburg]

Alternately, there seems to be nothing about cubic number fields, and I would enjoy adding that

[Notification Bot]

This topic was moved here from #general > autoformatter for lean by Scott Morrison

[Scott Morrison]

@Alex Meiburg there's lots of stuff missing! Hopefully some of people contributing recently to algebraic number theory like @Anne Baanen and @Chris Hughes will stop by to confirm, but I suspect you are correct on both points.

[Scott Morrison]

And yes, this sort of stuff is very welcome, and good material to get your teeth into Lean with!

[Alex Meiburg]

(oops, new to Zulip, I accidentially dropped this in the wrong channel -- my bad)

[Alex Meiburg]

Good to know Scott, thanks! :)