mathlib

6b15eb29 - chore(analysis): put lemmas in normed_field namespace (#1517)

chore(analysis): put lemmas in normed_field namespace (#1517) The motivation is to be able to state, say norm_mul for subrings of a normed field, typically p-adic integers. That way we can have padic_int.norm_mul, open the padic_int namespace and have no ambiguous name.