instNonarchimedeanRingCompletion — Mathlib

English

If R is a nonarchimedean ring, then its completion is a nonarchimedean ring.

Русский

Если R — неархимедово кольцо, то его завершение тоже неархимедово кольцо.

LaTeX

$$$\operatorname{NonarchimedeanRing}(R) \Rightarrow \operatorname{NonarchimedeanRing}(\mathrm{Completion}(R))$$$

Lean4

/-- The completion of a nonarchimedean ring is a nonarchimedean ring. -/
instance {R : Type*} [Ring R] [UniformSpace R] [IsTopologicalRing R] [IsUniformAddGroup R] [NonarchimedeanRing R] :
    NonarchimedeanRing (Completion R) where is_nonarchimedean := NonarchimedeanAddGroup.is_nonarchimedean

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