mathlib

60570d5b - chore(analysis/inner_product_space/basic): add a helper lemma