Commit 2026-03-05 11:23 9e7dfb2c

fix(NumberTheory/Padics): remove diamond normed instance on C_p (#36118) In this PR, we refactor the normed instance on $\mathbb{C}_p$ to the norm extended along completion, and show that this is compatible with valuation. Also added NontriviallyNormedField and CharZero instances. Before this PR, there were two non-defeq normed instance on $\mathbb{C}_p$.

1. Induced by UniformSpace.Completion.instNorm from the norm on the algebraic closure of Q_p,
2. Converted from Valued.norm from the valuation on $\mathbb{C}_p$. We choose the first one and show that it is propositionally equal to the second one as a theorem.