mathlib

ce79a27b - feat(analysis/normed_space/pi_Lp): add lemmas about `pi_Lp.equiv` (#13569)

feat(analysis/normed_space/pi_Lp): add lemmas about `pi_Lp.equiv` (#13569) Most of these are trivial `dsimp` lemmas, but they also let us talk about the norm of constant vectors.