Commit 2025-10-10 10:01 61e5c4c0

View on Github →

style: fix capitalisation Valued.isOpen_closedball -> Valued.isOpen_closedBall (#30358)

Estimated changes

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

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

added theorem Valued.isOpen_closedBall

deleted theorem Valued.isOpen_closedball