Theorem IsValuativeTopology.mem_nhds

Modification history

2025-08-04 23:21
Mathlib/Topology/Algebra/Valued/ValuativeRel.lean
chore(RingTheory/Valuation): change definition of IsValuativeTopology (#27939)
Deleted IsValuativeTopology.mem_nhdsView on Github →
2025-08-04 14:14
Mathlib/Topology/Algebra/Valued/ValuativeRel.lean
chore: rename ValuativeTopology to IsValuativeTopology (#26845)
Added IsValuativeTopology.mem_nhdsView on Github →