mathlib

e33245ca - feat(topology/metric_space/pi_Lp): L^p distance on finite products (#3059)

feat(topology/metric_space/pi_Lp): L^p distance on finite products (#3059) `L^p` edistance (or distance, or norm) on finite products of emetric spaces (or metric spaces, or normed groups), put on a type synonym `pi_Lp p hp α` to avoid instance clashes, and being careful to register as uniformity the product uniformity.