isLocalRing — Mathlib

English

The comap of the maximal ideal of Localization.AtPrime I equals I; i.e., the maximal ideal lies over I.

Русский

Обратное образ максимального идеала Localization.AtPrime I равно I; т. е. максимальный идеал лежит над I.

LaTeX

$$$$ \operatorname{Ideal.comap}(\operatorname{algebraMap} R (Localization.AtPrime I)) (\operatorname{IsLocalRing.maximalIdeal}(Localization I.primeCompl)) = I $$$$

Lean4

/-- The localization of `R` at the complement of a prime ideal is a local ring. -/
instance isLocalRing : IsLocalRing (Localization P.primeCompl) :=
  IsLocalization.AtPrime.isLocalRing (Localization P.primeCompl) P

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