# Commit 2021-06-19 15:31 cd8f7b5c

View on Github →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.