English
The image of I under the algebra map to Localization.AtPrime I is the maximal ideal of that localized ring.
Русский
Образ I под алгебраическому отображению в Localization.AtPrime I является максимальным идеалом этого локализованного кольца.
LaTeX
$$$$ \operatorname{Ideal.map}(\operatorname{algebraMap} R (Localization.AtPrime I)) I = \operatorname{IsLocalRing.maximalIdeal}(Localization I.primeCompl) $$$$
Lean4
instance {R S : Type*} [CommRing R] [NoZeroDivisors R] {P : Ideal R} [CommRing S] [Algebra R S] [NoZeroSMulDivisors R S]
[IsDomain S] [P.IsPrime] :
NoZeroSMulDivisors (Localization.AtPrime P) (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
NoZeroSMulDivisors_of_isLocalization R S _ _ P.primeCompl_le_nonZeroDivisors
