Gauss Lemma and Eisenstein's Criterion

Stream: maths

[Aditya Agarwal]

Is anyone working on Gauss Lemma and Eisenstein's Criterion or are they present in mathlib?

[Kenny Lau]

@Chris Hughes What do you think

[Kevin Buzzard]

I believe general UFDs are in mathlib nowadays, so anyone who implements them should probably do it in this generality.

[Kevin Buzzard]

although I guess Rob Lewis proved all the stuff about valuations for the integers when defining the p-adic numbers, and it might even be the case that the basic theory of valuations for a general UFD is not done (athough it might be a fairly simple port from Rob's work on Z)

[Johan Commelin]

@Aditya Agarwal Cool, I'm currently writing exercise sheets for 2nd year students who have to practice with Gauss Lemma and Eisenstein. It would be awesome if that lands in mathlib!

[Kevin Buzzard]

https://github.com/leanprover/mathlib/blob/master/data/padics/padic_norm.lean The first 370 or so lines of that file are the basics of the p-adic valuation on the integers and rationals. That should all be ported to a general UFD really, if one is to do this properly. One needs it in the proofs of such things as R a UFD -> R[X] a UFD.