localRingLocalizations — Mathlib

English

For every prime P in the topological spectrum of R, the localization of R at P is a local ring.

Русский

Для каждого простого идеала P на спектре R локализация R в P образует локальное кольцо.

LaTeX

$$$\\forall P \\in \\mathrm{PrimeSpectrum.Top}\\, R,\\; \\operatorname{Localizations} R P \\text{ is local.}$$$

Lean4

instance localRingLocalizations (P : PrimeSpectrum.Top R) : IsLocalRing <| Localizations R P :=
  inferInstanceAs <| IsLocalRing <| Localization.AtPrime P.asIdeal

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