IsReduced is a local property

In this file, we prove that IsReduced is a local property.

Main results

Let R be a commutative ring, M be a submonoid of R.

• isReduced_localizationPreserves : M⁻¹R is reduced if R is reduced.
• isReduced_ofLocalizationMaximal : R is reduced if Rₘ is reduced for all maximal ideal m.

theorem isReduced_localizationPreserves : LocalizationPreserves fun (R : Type u_1) (x : CommRing R) => IsReduced R

M⁻¹R is reduced if R is reduced.

instance instIsReducedLocalization {R : Type u_1} [CommRing R] (M : Submonoid R) [IsReduced R] : IsReduced (Localization M)

theorem isReduced_ofLocalizationMaximal : OfLocalizationMaximal fun (R : Type u_1) (x : CommRing R) => IsReduced R

R is reduced if Rₘ is reduced for all maximal ideal m.