mathlib

59a1a509 - chore(analysis/normed_space/pi_Lp): add `pi_Lp.linear_equiv` (#14380)

chore(analysis/normed_space/pi_Lp): add `pi_Lp.linear_equiv` (#14380) This is just a more bundled version of the `pi_Lp.equiv` we already have. Also adds two missing simp lemmas about `pi_Lp.equiv`.