Theorems · Theorem · commutative algebra

Polynomial.isIntegral_coeff_of_dvd

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Polynomial R)
  (q : Polynomial S), p.Monic → q.Monic → q ∣ Polynomial.map (algebraMap R S) p → ∀ (i : ℕ), IsIntegral R (q.coeff i)

[Stacks Tag 00H6](https://stacks.math.columbia.edu/tag/00H6) ((1))

Defined in

Mathlib.RingTheory.Polynomial.IsIntegral

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra