Commit 2021-09-30 02:06 f254c2f8
View on Github →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