adicCompletionIntegers — Mathlib

English

The adic completion carries an intrinsic ring of integers substructure, defined as the valuation subring of the adic completion.

Русский

Завершение по адической норме содержит внутреннее множество целых чисел — подкольцо оценки завершения.

LaTeX

$$adicCompletionIntegers (v) is a valuation subring of (v.adicCompletion K)$$

Lean4

/-- The ring of integers of `adicCompletion`. -/
def adicCompletionIntegers : ValuationSubring (v.adicCompletion K) :=
  Valued.v.valuationSubring

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