mathlib

2fb109f0 - feat(analysis/inner_product/orientation, geometry/euclidean/oriented_angle): use bundled orthonormal bases (#16475)

feat(analysis/inner_product/orientation, geometry/euclidean/oriented_angle): use bundled orthonormal bases (#16475) Bundled orthonormal bases (as opposed to bases with a mixin predicate `orthonormal`) were defined in #12060, and some of the use cases were switched over in #12253. This PR completes the job, switching to bundled orthonormal bases in `inner_product/orientation` and `euclidean/oriented_angle` as well as in one remaining construction (the standard ` ℝ`-orthonormal basis of `ℂ`) in `inner_product/pi_L2`. Formalized as part of the Sphere Eversion project. The part that I will be using in future PRs is the bundled version of the construction `orthonormal_basis.adjust_to_orientation` in `inner_product/orientation`.