mathlib3

feat(analysis/inner_product_space/l2_space.lean): collect Hilbert bases along a Hilbert sum decomposition

#15791

Open