ofPrime — Mathlib

English

The localization of a subring at a prime, as a local subring.

Русский

Локализация подкольца по простому идеалу, как локальное подполь кольцо.

LaTeX

$$ofPrime(A,P) is a LocalSubring K (localization at prime).$$

Lean4

/-- The localization of a subring at a prime, as a local subring.
Also see `Localization.subalgebra.ofField` -/
noncomputable def ofPrime (A : Subring K) (P : Ideal A) [P.IsPrime] : LocalSubring K :=
  range
    (IsLocalization.lift (M := P.primeCompl) (S := Localization.AtPrime P) (g := A.subtype)
      (by simp [Ideal.primeCompl, not_imp_not]))

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