Commit 2022-08-09 20:13 b6ab1f47

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. 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.