Zulip Chat Archive

Stream: maths

Topic: hensel


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?

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.

Johan Commelin (Feb 28 2019 at 08:46):

Sure, I understand why the other files are there.

Johan Commelin (Feb 28 2019 at 08:46):

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

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: Dec 20 2023 at 11:08 UTC