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.

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.

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯