Theorem NonarchimedeanGroup.prod_self_subset

Modification history

2024-02-11 18:26
Mathlib/Topology/Algebra/Nonarchimedean/Basic.lean
chore(*): use notation for nhds (#10416) …
Modified NonarchimedeanGroup.prod_self_subsetView on Github →
2023-03-17 16:27
Mathlib/Topology/Algebra/Nonarchimedean/Basic.lean
feat: port Topology.Algebra.Nonarchimedean.Basic (#2958)
Added NonarchimedeanGroup.prod_self_subsetView on Github →