isFractionRing — Mathlib

English

If a valuation v has integers 𝒪 (hv), then 𝒪 is a fraction ring of K.

Русский

Если оценка v имеет целые 𝒪 (hv), то 𝒪 является дробно-кольцом K.

LaTeX

$$$IsFractionRing 𝒪 K$$$

Lean4

theorem _root_.Valuation.Integers.isFractionRing {v : Valuation K Γ} (hv : v.Integers 𝒪) : IsFractionRing 𝒪 K :=
  isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective hv.eq_algebraMap_or_inv_eq_algebraMap
    hv.hom_inj

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