instIsFractionRing — Mathlib

English

If S is a field of fractions of R and v is a valuation on R, then WithVal v has a natural fraction-field relation with S: IsFractionRing S (WithVal v).

Русский

Если S является полем дробей R, и v — оценка на R, то для WithVal v верна структура поля дробей: IsFractionRing S (WithVal v).

LaTeX

$$$IsFractionRing S (WithVal v)$$$

Lean4

instance [CommRing S] [CommRing R] [Algebra S R] [IsFractionRing S R] (v : Valuation R Γ₀) :
    IsFractionRing S (WithVal v) :=
  inferInstanceAs (IsFractionRing S R)

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