refactor(*): rename `nondiscrete_normed_field` (#15625)
This renames `nondiscrete_normed_field` to `nontrivially_normed_field` in accordance with this [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/hypotheses.20for.20a.20field.20property/near/290408091)
