Commit 2020-10-01 18:43 48518578

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 lists and finsets.