Commit 2025-10-06 08:23 afc966d8

View on Github →

feat(Topology/WithVal): ValuativeRel (WithVal v) (#27207) with a helper valuation defined that does not pierce defeq

Estimated changes

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

added def WithVal.valuation

added theorem WithVal.valuation_equiv_symm