mathlib

51ad06e5 - refactor(analysis/inner_product_space/*): split big file (#9382)

refactor(analysis/inner_product_space/*): split big file (#9382) This PR makes a new folder `analysis/inner_product_space/*` comprising several files splitting the old `analysis/normed_space/inner_product` (which had reached 2900 lines!). https://leanprover.zulipchat.com/#narrow/stream/116395-maths