Theorem IsValuativeTopology.hasBasis_nhds_zero'

Modification history

2025-10-05 10:04
Mathlib/Topology/Algebra/Valued/ValuativeRel.lean
feat: the definition of nonarchimedean local fields (#27465)
Added IsValuativeTopology.hasBasis_nhds_zero'View on Github →