mathlib3

3feacfe6 - chore(analysis/normed_space/pi_Lp): add `pi_Lp.linear_equiv`

chore(analysis/normed_space/pi_Lp): add `pi_Lp.linear_equiv` 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`.