mathlib3

b6ab1f47 - feat(analysis/normed/field/basic): define `densely_normed_field` give instances for ℚ, ℝ, ℂ and `is_R_or_C` (#15657)

feat(analysis/normed/field/basic): define `densely_normed_field` give instances for ℚ, ℝ, ℂ and `is_R_or_C` (#15657) This adds a new type class extending `normed_field` which is named `densely_normed_field` per this [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/hypotheses.20for.20a.20field.20property/near/290408091). The name comes from the fact that the (nn)norm has dense range in ℝ≥0. This type class is strictly stronger than `nontrivially_normed_field`, with `padic` being a field which is nontrivially normed but not densely normed. The instances of `nontrivially_normed_field` for each of ℚ, ℝ, ℂ have all been migrated to `densely_normed_field` instead. Moreover, `is_R_or_C` now extends `densely_normed_field`; this is natural because even if it only extends `nontrivially_normed_field`, it would still be possible to prove that the norm has dense range in ℝ≥0.