mathlib

9ed71796 - refactor(*): move normed field lemmas into root namespace (#12163)

refactor(*): move normed field lemmas into root namespace (#12163) This takes the normed field lemmas given in `analysis.normed_space.basic` and moves them from the `normed_field` namespace into the root namespace. This PR moves these lemmas and definitions: `norm_mul`, `nnnorm_mul`, `norm_hom`, `nnnorm_hom`, `norm_pow`, `nnnorm_pow`, `norm_prod`, `nnnorm_prod`, `norm_div`, `nnnorm_div`, `norm_inv`, `nnnorm_inv`, `norm_zpow`, `nnnorm_zpow`.