mathlib

f435f954 - feat(analysis/inner_product_space): ext lemmas for dense subspaces (#17450)