Commit 2024-05-13 09:51 3844ad73

feat: completion of a nonarchimedean additive group (#12669) We prove that the completion of a nonarchimedean additive group is a nonarchimedean additive group. Detailed comments are included because I could not find a proof in the literature anywhere.