Def IsUltrametricDist.ball_openSubgroup

Modification history

2024-10-04 11:14
Mathlib/Analysis/Normed/Group/Ultra.lean
feat (Analysis/Normed/Group): ultrametric normed groups are nonarchimedean (#17262) …
Added IsUltrametricDist.ball_openSubgroupView on Github →