Gauss's Lemma for Dedekind Domains

This file contains Gauss's Lemma for Dedekind Domains, which states that the content ideal of a polynomial is the whole ring if and only if the v-adic Gauss norms of the polynomial are equal to 1 for all v.

theorem Polynomial.gaussNorm_intAdicAbv_le_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) (p : Polynomial R) : gaussNorm (v.intAdicAbv hb) 1 p ≤ 1

theorem Polynomial.gaussNorm_lt_one_iff_contentIdeal_le {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) (p : Polynomial R) : gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal

Given a polynomial p in R[X], the v-adic Gauss norm of p is smaller than 1 if and only if the content ideal of p is contained in the prime ideal corresponding to v.

theorem Polynomial.contentIdeal_eq_top_iff_forall_gaussNorm_eq_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {b : NNReal} (hb : 1 < b) (p : Polynomial R) (hR : ¬IsField R) : p.contentIdeal = ⊤ ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1

Gauss's Lemma: given a polynomial p in R[X], the content ideal of p is the whole ring if and only if the v-adic Gauss norms of p are equal to 1 for all v.

theorem Polynomial.isPrimitive_iff_forall_gaussNorm_eq_one {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (hR : ¬IsField R) {b : NNReal} (hb : 1 < b) (p : Polynomial R) : p.IsPrimitive ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1

In case R is PID, given a polynomial p in R[X], p is primitive if and only if the v-adic Gauss norms of p are equal to 1 for all v.