mathlib

be61b02b - chore(analysis/normed/group/basic): Earlier `ℝ` lemmas (#16972)

chore(analysis/normed/group/basic): Earlier `ℝ` lemmas (#16972) Move lemmas about the norm on `ℝ` from `analysis.normed.field.basic` to `analysis.normed.group.basic`. This avoids having to import `normed_field` to use `real.norm_of_nonneg`.