mathlib

f254c2f8 - refactor(analysis/normed_space/{dual, pi_Lp}): split out inner product space parts (#9388)

refactor(analysis/normed_space/{dual, pi_Lp}): split out inner product space parts (#9388) This is just moving code, no math changes. https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/New.20folder.20analysis.2Finner_product_space