Zulip Chat Archive

Stream: maths

Topic: hensel


view this post on Zulip Johan Commelin (Feb 28 2019 at 07:12):

Yesterday I was trying to find Hensel's lemma, and I was somewhat surprised to find it under data/. I would have expected that theorems and lemmas about the padics would be in ring_theory/ or something like that. Is there a reason to put Hensel's lemma in data/, or is it just there because all the other p-adic stuff is there as well?

view this post on Zulip Rob Lewis (Feb 28 2019 at 08:45):

No good reason. The other padic files are just as much data as data.real is data, and they all went in the same directory.

view this post on Zulip Johan Commelin (Feb 28 2019 at 08:46):

Sure, I understand why the other files are there.

view this post on Zulip Johan Commelin (Feb 28 2019 at 08:46):

Anyway, doesn't matter too much to me. Only trying to understand the conventions.

view this post on Zulip Mario Carneiro (Feb 28 2019 at 15:06):

I think data.padic.basic should set up the type itself, and the operations, and prove it's a field etc., and everything else should go in another folder, like number_theory or ring_theory


Last updated: May 18 2021 at 08:14 UTC