Theorems · Theorem · commutative algebra

Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map

∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [IsDomain R] [IsGCDMonoid R] {p : Polynomial R},
  p.IsPrimitive → (Irreducible p ↔ Irreducible (Polynomial.map (algebraMap R K) p))

Gauss's Lemma for GCD domains states that a primitive polynomial is irreducible iff it is irreducible in the fraction field.

Defined in

Mathlib.RingTheory.Polynomial.GaussLemma

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebraIsFractionRingIsDomainIsGCDMonoid