Commit 2025-04-16 22:42 3821c1d2
View on Github →chore(Topology.Algebra.Valued.WithVal): clean up typeclass assumptions (#24125)
Currently WithVal.instCommRing has Ring R and CommRing R both in the context resulting in Valuation using the Ring R instance the statement and the CommRing R instance for the body after unwrapping WithVal. Other wrapper instances are fixed similarly.