hensel

Stream: maths

[Johan Commelin]

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]

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]

Sure, I understand why the other files are there.

[Johan Commelin]

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

[Mario Carneiro]

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