Theorems · Theorem · commutative algebra

IsIntegrallyClosed.eq_map_mul_C_of_dvd

∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [IsIntegrallyClosed R] {f : Polynomial R},
  f.Monic →
    ∀ {g : Polynomial K},
      g ∣ Polynomial.map (algebraMap R K) f → ∃ g', Polynomial.map (algebraMap R K) g' * Polynomial.C g.leadingCoeff = g

If K = Frac(R) and g : K[X] divides a monic polynomial with coefficients in R, then g * (C g.leadingCoeff⁻¹) has coefficients in R

Defined in

Mathlib.RingTheory.Polynomial.GaussLemma

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebraIsFractionRingIsIntegrallyClosed