mathlib3

9dffb788 - fix(analysis/normed_space/pi_Lp): remove bad simp lemmas for `pi_Lp.equiv` (#17327)

fix(analysis/normed_space/pi_Lp): remove bad simp lemmas for `pi_Lp.equiv` (#17327) This regression was introduced in #14231. These lemmas are a bad idea for the same reason that a lemma stating `multiplicative.of_add x = x` would be; it discards the type information that is the sole reason for the existance of the `def`! This also adds a new `pi_Lp.basis_fun` which is the `pi_Lp` version of `pi.basis_fun`.