Normed instance on `C_p`

Stream: mathlib4

[Jiang Jiedong]

Currently, there are two non-defeq normed instance on $C_p$. The first one is PadicComplex.instNormedField converted from PadicComplex.valued, the second is UniformSpace.Completion.instNormedSpace, which have more prebuilt APIs. This conflict between instances is blocking further developments like proving Krasner's lemma and C_pis not spherically complete.

I propose the following potential solution. First we define a class ValuedNormed extending both Valued and Normed as discussed with @Johan Commelin a long time ago, assuming the valuation is compatible with the norm (i.e. v x < v y, iff |x| > |y|). Then establish an instance of C_p of this class, using the norm defined by UniformSpace.Completion.instNormedSpace.

Does anyone have other possible solutions or suggestions? Thank you!

[Yury G. Kudryashov]

Since Valued.toNormedField is a def, you can just change docs#PadicComplex.instNormedField to use docs#UniformSpace.Completion.instNormedSpace, then prove that it agrees with the valuation, if needed.

[Kevin Buzzard]

Why not just delete PadicComplex.instNormedField? (oh sorry, that's what Yury is saying)

[Jiang Jiedong]

Thanks! I’ll try the deletion option.