Theorems · Theorem · commutative algebra

Polynomial.gaussNorm_lt_one_iff_contentIdeal_le

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  {b : NNReal} (hb : 1 < b) (p : Polynomial R),
  Polynomial.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.

Defined in

Mathlib.RingTheory.DedekindDomain.GaussLemma

Cited by

0 results in Mathlib

Foundations

Depth 157 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDedekindDomain