Commit 2025-08-04 14:14 2c0fd5ce

View on Github →

chore: rename ValuativeTopology to IsValuativeTopology (#26845)

Estimated changes

Modified Mathlib/RingTheory/Valuation/ValuativeRel.lean

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

added theorem IsValuativeTopology.hasBasis_nhds_zero

added theorem IsValuativeTopology.isClopen_ball

added theorem IsValuativeTopology.isClopen_closedBall

added theorem IsValuativeTopology.isClopen_sphere

added theorem IsValuativeTopology.isClosed_ball

added theorem IsValuativeTopology.isClosed_closedBall

added theorem IsValuativeTopology.isOpen_ball

added theorem IsValuativeTopology.isOpen_closedBall

added theorem IsValuativeTopology.isOpen_sphere

added theorem IsValuativeTopology.mem_nhds

deleted theorem ValuativeTopology.hasBasis_nhds_zero

deleted theorem ValuativeTopology.isClopen_ball

deleted theorem ValuativeTopology.isClopen_closedBall

deleted theorem ValuativeTopology.isClopen_sphere

deleted theorem ValuativeTopology.isClosed_ball

deleted theorem ValuativeTopology.isClosed_closedBall

deleted theorem ValuativeTopology.isOpen_ball

deleted theorem ValuativeTopology.isOpen_closedBall

deleted theorem ValuativeTopology.isOpen_sphere

deleted theorem ValuativeTopology.mem_nhds