# Zulip Chat Archive

## Stream: maths

### Topic: Gauss Lemma and Eisenstein's Criterion

#### Aditya Agarwal (Nov 13 2018 at 00:02):

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

#### Kenny Lau (Nov 13 2018 at 00:02):

@Chris Hughes What do you think

#### Kevin Buzzard (Nov 13 2018 at 00:06):

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

#### Kevin Buzzard (Nov 13 2018 at 00:08):

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 (Nov 13 2018 at 08:12):

@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 (Nov 13 2018 at 08:16):

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.

Last updated: May 11 2021 at 15:12 UTC