mathlib

e9f2a838 - chore(analysis/normed_space/pi_Lp): add `pi_Lp.continuous_linear_equiv` (#19014)

chore(analysis/normed_space/pi_Lp): add `pi_Lp.continuous_linear_equiv` (#19014) This bundling is often useful to have. We keep around `pi_Lp.linear_equiv` as this is shorter to write than `pi_Lp.continuous_linear_equiv.to_linear_equiv`.