Results about coefficients of polynomials being integral

Main results

• Polynomial.isIntegral_coeff_of_dvd: If a monic polynomial p divides another monic polynomial with integral coefficients, then the coefficients of p are themselves integral.
• Polynomial.isIntegral_iff_isIntegral_coeff: p : S[X] is integral over R[X] iff the coefficients of p are integral over R.
• MvPolynomial.isIntegral_iff_isIntegral_coeff: p : MvPolynomial σ S is integral over MvPolynomial σ R iff the coefficients of p are integral over R.
• We also provide the instance [IsIntegrallyClosed R] : IsIntegrallyClosed R[X].

theorem Polynomial.isIntegral_coeff_prod {R : Type u_1} {S : Type u_2} {ι : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (s : Finset ι) (p : ι → Polynomial S) (H : ∀ i ∈ s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) (j : ℕ) : IsIntegral R ((s.prod p).coeff j)

theorem Polynomial.isIntegral_coeff_of_factors {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Polynomial S) (hpmon : IsIntegral R p.leadingCoeff) (hp : p.Splits) (hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x) (i : ℕ) : IsIntegral R (p.coeff i)

theorem Polynomial.isIntegral_coeff_of_dvd {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Polynomial R) (q : Polynomial S) (hp : p.Monic) (hq : q.Monic) (H : q ∣ map (algebraMap R S) p) (i : ℕ) : IsIntegral R (q.coeff i)

Stacks Tag 00H6 ((1))

theorem IsAlmostIntegral.coeff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [FaithfulSMul R S] {p : Polynomial S} (hp : IsAlmostIntegral (Polynomial R) p) (i : ℕ) : IsAlmostIntegral R (p.coeff i)

Stacks Tag 00H0 ((1))

theorem IsIntegral.coeff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {p : Polynomial S} (hp : IsIntegral (Polynomial R) p) (i : ℕ) : IsIntegral R (p.coeff i)

Stacks Tag 00H0 ((2))

@[deprecated IsIntegral.coeff (since := "2026-01-01")]

theorem IsIntegral.coeff_of_exists_smul_mem_lifts {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {p : Polynomial S} (hp : IsIntegral (Polynomial R) p) (i : ℕ) : IsIntegral R (p.coeff i)

Alias of IsIntegral.coeff.

---

Stacks Tag 00H0 ((2))

@[deprecated IsIntegral.coeff (since := "2026-01-01")]

theorem IsIntegral.coeff_of_isFractionRing {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {p : Polynomial S} (hp : IsIntegral (Polynomial R) p) (i : ℕ) : IsIntegral R (p.coeff i)

Alias of IsIntegral.coeff.

---

Stacks Tag 00H0 ((2))

theorem Polynomial.isIntegral_iff_isIntegral_coeff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {f : Polynomial S} : IsIntegral (Polynomial R) f ↔ ∀ (n : ℕ), IsIntegral R (f.coeff n)

theorem IsIntegral.of_aeval_monic_of_isIntegral_coeff {R : Type u_4} {A : Type u_5} [CommRing R] [CommRing A] [Algebra R A] {x : A} {p : Polynomial A} (monic : p.Monic) (deg : p.natDegree ≠ 0) (hx : IsIntegral R (Polynomial.eval x p)) (hp : ∀ (i : ℕ), IsIntegral R (p.coeff i)) : IsIntegral R x

instance instIsIntegrallyClosedPolynomialOfIsDomain {R : Type u_4} [CommRing R] [IsDomain R] [IsIntegrallyClosed R] : IsIntegrallyClosed (Polynomial R)

Stacks Tag 030A

theorem MvPolynomial.isIntegral_iff_isIntegral_coeff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {σ : Type w} {f : MvPolynomial σ S} : IsIntegral (MvPolynomial σ R) f ↔ ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)