isReduced_ofLocalizationMaximal — Mathlib

English

R is reduced if all maximal localizations are reduced.

Русский

R редуцировано, если все локализации по максимуму редуцированы.

LaTeX

$$$\\text{OfLocalizationMaximal }( \\text{IsReduced} )$$$

Lean4

/-- `R` is reduced if `Rₘ` is reduced for all maximal ideal `m`. -/
theorem isReduced_ofLocalizationMaximal : OfLocalizationMaximal fun R _ => IsReduced R :=
  by
  introv R h
  constructor
  intro x hx
  apply eq_zero_of_localization
  intro J hJ
  specialize h J hJ
  exact (hx.map <| algebraMap R <| Localization.AtPrime J).eq_zero

Похожие утверждения