mathlib

72498958 - feat(analysis/inner_product_space/basic): negating orthonormal vectors (#11208)

feat(analysis/inner_product_space/basic): negating orthonormal vectors (#11208) Add a lemma that, given an orthonormal family, negating some of the vectors in it produces another orthonormal family.