Documentation

Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected

Total separatedness of nonarchimedean groups #

In this file, we prove that a nonarchimedean group is a totally separated topological space. The fact that a nonarchimedean group is a totally disconnected topological space is implied by the fact that a nonarchimedean group is totally separated.

Main results #

Notation #

References #

See Proposition 2.3.9 and Problem 63 in [F. Q. Gouvêa, p-adic numbers][gouvea1997].