`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.

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`

.