mathlib3

cd8f7b5c - chore(topology/metric_space/pi_Lp): move to analysis folder, import inner_product_space (#7991)

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.