Documentation

Mathlib.Topology.Algebra.Nonarchimedean.Completion

The completion of a nonarchimedean additive group #

The completion of a nonarchimedean additive group is a nonarchimedean additive group.

The completion of a nonarchimedean ring is a nonarchimedean ring.

source
instance instNonarchimedeanAddGroupCompletion {G : Type u_1} [AddGroup G] [UniformSpace G] [UniformAddGroup G] [NonarchimedeanAddGroup G] :
NonarchimedeanAddGroup (UniformSpace.Completion G)

The completion of a nonarchimedean additive group is a nonarchimedean additive group.

source
instance instNonarchimedeanRingCompletion {R : Type u_1} [Ring R] [UniformSpace R] [TopologicalRing R] [UniformAddGroup R] [NonarchimedeanRing R] :
NonarchimedeanRing (UniformSpace.Completion R)

The completion of a nonarchimedean ring is a nonarchimedean ring.