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.