mathlib

91b5bdde - feat(analysis/normed_space/lp_equiv): equivalences between `lp` and `pi_Lp`, `bounded_continuous_function` (#15872)

feat(analysis/normed_space/lp_equiv): equivalences between `lp` and `pi_Lp`, `bounded_continuous_function` (#15872) This adds a new file for equivalences between various L^p spaces. We do this in a new file instead of `analysis/normed_space/lp_space` in order to minimize imports. We begin by establishing the equivalence between `lp` and `pi_Lp` when the index type is a fintype, and then proceed to recognize the equivalence between `lp` (for `p = ∞`) and `bounded_continuous_function` when the codomain has various algebraic structures. - [x] depends on: #15833 - [x] depends on: #15852