Commit 2019-10-08 15:54 6b15eb29

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.