Commit 2022-02-21 15:30 9ed71796

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.