Polynomial over Regular Ring

In this file we prove that the polynomial ring over a regular ring is regular.

Main results

• Polynomial.isRegularRing_of_isRegularRing : the polynomial ring over a regular ring is a regular ring.

• MvPolynomial.isRegularRing_of_isRegularRing : the multivariate polynomial ring with finite variates over a regular ring is a regular ring.

theorem Polynomial.isRegularLocalRing_localization_atPrime_of_comap_eq_maximalIdeal (R : Type u_1) [CommRing R] [IsRegularLocalRing R] (p : Ideal (Polynomial R)) [p.IsPrime] (max : Ideal.comap C p = IsLocalRing.maximalIdeal R) : IsRegularLocalRing (Localization.AtPrime p)

instance Polynomial.isRegularRing_of_isRegularRing (R : Type u_1) [CommRing R] [IsRegularRing R] : IsRegularRing (Polynomial R)

instance MvPolynomial.isRegularRing_of_isRegularRing (R : Type u_1) [CommRing R] [IsRegularRing R] {ι : Type u_2} [Finite ι] : IsRegularRing (MvPolynomial ι R)