Commit 2022-11-09 17:39 9dffb788

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.