Results about coefficients of polynomials being integral

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] [IsDomain S] (p : Polynomial S) (hpmon : IsIntegral R p.leadingCoeff) (hp : p.Splits) (hpr : ∀ x ∈ p.roots, 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] [IsDomain S] (p : Polynomial R) (q : Polynomial S) (hp : p.Monic) (hq : IsIntegral R q.leadingCoeff) (H : q ∣ map (algebraMap R S) p) (i : ℕ) : IsIntegral R (q.coeff i)

Stacks Tag 00H6 ((1))