valuationRing — Mathlib

English

If f: R →+* S is surjective and R has a pre-valuation ring, then S is a valuation ring.

Русский

Если f: R →+* S сюръективно, и R обладает структурой предвалюационного кольца, то S является валюационным кольцом.

LaTeX

$$$\\text{ValuationRing } S$$$

Lean4

theorem _root_.Function.Surjective.valuationRing {R S : Type*} [NonAssocSemiring R] [PreValuationRing R] [CommRing S]
    [IsDomain S] (f : R →+* S) (hf : Function.Surjective f) : ValuationRing S :=
  have : PreValuationRing S := Function.Surjective.preValuationRing (R := R) f hf
  .mk

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