Theorem IsValuativeTopology.hasBasis_nhds'

Modification history

2026-03-21 18:59

Mathlib/Topology/Algebra/ValuativeRel/ValuativeTopology.lean

feat(Valued/ValuationTopology): Add and generalize lemmas for `IsValuativeTopology` (#36532) …

Modified IsValuativeTopology.hasBasis_nhds'View on Github →

2025-10-05 10:04

Mathlib/Topology/Algebra/Valued/ValuativeRel.lean

feat: the definition of nonarchimedean local fields (#27465)

Added IsValuativeTopology.hasBasis_nhds'View on Github →