instIsFractionRingInteger — Mathlib

English

Let v be a valuation on a field K with value group Γ. The subring O_v = v.integer (the integers with respect to v) has field of fractions equal to K; equivalently, K is the fraction field of O_v.

Русский

Пусть v — валиация на поле K с группой значений Γ. Подкольцо O_v = v.integer (целые относительно v) обладает полем дробей, равным K; эквивалентно, K является полем дробей над O_v.

LaTeX

$$$K \cong \operatorname{Frac}(\mathcal{O}_v), \quad \mathcal{O}_v = \{ x \in K : v(x) \ge 0 \}$$$

Lean4

instance instIsFractionRingInteger (v : Valuation K Γ) : IsFractionRing v.integer K :=
  (Valuation.integer.integers v).isFractionRing

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