Going down for integrally closed domains

In this file, we provide the instance that any integral extension of R ⊆ S satisfies going down if R is integrally closed.

theorem Polynomial.coeff_mem_radical_span_coeff_of_dvd {R : Type u_1} [CommRing R] (p q : Polynomial R) (hp : p.Monic) (hq : q.Monic) (H : q ∣ p) (i : ℕ) (hi : i ≠ q.natDegree) : q.coeff i ∈ (Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x}).radical

instance instHasGoingDownOfIsDomainOfFaithfulSMulOfIsIntegralOfIsIntegrallyClosed {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain S] [FaithfulSMul R S] [Algebra.IsIntegral R S] [IsIntegrallyClosed R] : Algebra.HasGoingDown R S

Stacks Tag 00H8