Commit 2025-08-04 23:21 b24ea323

View on Github →

chore(RingTheory/Valuation): change definition of IsValuativeTopology (#27939)

Estimated changes

Modified Mathlib/RingTheory/Valuation/ValuativeRel.lean

Modified Mathlib/Topology/Algebra/Valued/ValuativeRel.lean

added theorem IsValuativeTopology.hasBasis_nhds

deleted theorem IsValuativeTopology.mem_nhds

added theorem IsValuativeTopology.mem_nhds_iff'

added theorem IsValuativeTopology.mem_nhds_zero_iff

added theorem IsValuativeTopology.of_zero