instIsLocalRingSubtypeMemSubringMapOfNontrivial

English

The localization of a subring at a prime is a local subring.

Русский

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

LaTeX

$$$\\text{ofPrime}(A,P)\\text{ is a local subring of }K$$$

Lean4

instance [Nontrivial S] (f : R →+* S) (s : Subring R) [IsLocalRing s] : IsLocalRing (s.map f) :=
  .of_surjective' (f.restrict s _ (fun _ ↦ Set.mem_image_of_mem f)) (fun ⟨_, a, ha, e⟩ ↦ ⟨⟨a, ha⟩, Subtype.ext e⟩)

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