Commit 2025-08-08 18:47 7036baf8

View on Github →

chore(Valued/WithVal): apply_symm_equiv (#27110) valuation on the WIthVal is equal to the underlying valuation and simp tag

Estimated changes

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

modified theorem WithVal.apply_equiv

added theorem WithVal.apply_symm_equiv