mathlib3

2642c89b - feat(analysis/inner_product_space/orientation): orientations of real inner product spaces (#11269)

feat(analysis/inner_product_space/orientation): orientations of real inner product spaces (#11269) Add definitions and lemmas relating to orientations of real inner product spaces, in particular constructing an orthonormal basis with a given orientation in finite positive dimension. This is in a new file since nothing else about inner product spaces needs to depend on orientations.