Commit 2021-06-19 15:31 cd8f7b5c

chore(topology/metric_space/pi_Lp): move to analysis folder, import inner_product_space (#7991) Currently, the file pi_Lp (on finite products of metric spaces, with the L^p norm) is in the topology folder, but it imports a lot of analysis (to have real powers) and it defines a normed space structure, so it makes more sense to have it in analysis. Also, it is currently imported by inner_product_space, to give an explicit construction of an inner product space on pi_Lp 2, which means that all files importing general purposes lemmas on inner product spaces also import real powers, trigonometry, and so on. We swap the imports, letting pi_Lp import inner_product_space and moving the relevant bits from the latter file to the former. This gives a more reasonable import graph.