chore(analysis/normed_space): define `norm_one_class` (#4323)
Many normed rings have `∥1⊫1`. Add a typeclass mixin for this property.
API changes:
* drop `normed_field.norm_one`, use `norm_one` instead;
* same with `normed_field.nnnorm_one`;
* new typeclass `norm_one_class` for `∥1∥ = 1`;
* add `list.norm_prod_le`, `list.norm_prod_le`, `finset.norm_prod_le`, `finset.norm_prod_le'`:
norm of the product of finitely many elements is less than or equal to the product of their norms;
versions with prime assume that a `list` or a `finset` is nonempty, while the other versions
assume `[norm_one_class]`;
* rename `norm_pow_le` to `norm_pow_le'`, new `norm_pow_le` assumes `[norm_one_class]` instead
of `0 < n`;
* add a few supporting lemmas about `list`s and `finset`s.
