Commit 2025-03-13 09:12 eeb4177a

View on Github →

feat: add to WithVal API (#22491) Upstream fixes to errors generated in FLT following the refactor of HeightOneSpectrum.adicCompletion in #22055

add additional instances to WithVal API
provide WithVal alternative to adicValued_apply

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

added theorem IsDedekindDomain.HeightOneSpectrum.adicValued_apply'

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