Commit 2026-03-02 19:44 fc35a055

View on Github →

chore: fix naming in WithVal (#35972) Minor cleanup post #34049

Estimated changes

Modified Mathlib/NumberTheory/Padics/WithVal.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

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

deleted theorem WithVal.apply_equiv

added theorem WithVal.apply_ofVal

deleted theorem WithVal.apply_symm_equiv

added theorem WithVal.valued_toVal