Commit 2025-08-19 04:15 a79ea2e6

View on Github →

chore: fix defeq abuse in WithVal (#28597) Follow-up after #27110

Estimated changes

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

modified theorem WithVal.apply_equiv

modified theorem WithVal.apply_symm_equiv