Theorems · Theorem · commutative algebra

Polynomial.isPrimitive_iff_forall_gaussNorm_eq_one

∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R],
  ¬IsField R →
    ∀ {b : NNReal} (hb : 1 < b) (p : Polynomial R),
      p.IsPrimitive ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum R), Polynomial.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.

Defined in

Mathlib.RingTheory.DedekindDomain.GaussLemma

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainIsPrincipalIdealRing