Commit 2024-10-22 04:01 fa9f767f

chore(Topology/Algebra/Valued/NormedValued): rely on TC IsUltrametricDist instead of explicit arg (#17561) Before, we had

[hK : NormedField K] (h : IsNonarchimedean (norm : K → ℝ))

Now we use [hK : NormedField K] [IsUltrametricDist K] to convert between ultrametrically normed fields and valued fields. This allows the instance to be a scoped instance instead of a def, since IsUltrametricDist is a class on the type, as opposed to a plain prop about the norm of the type. The instance is scoped because otherwise, one gets a TC loop.