mathlib3
feat(analysis/inner_product_space/finite_dimensional): some lemmas on finite dimensional inner product spaces
#18041
Open
Open