Commit 2022-01-10 23:30 2642c89b

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.