Commit 2022-02-27 14:12 00a3d02e

feat(geometry/euclidean/oriented_angle): oriented angles with respect to an orientation (#12236) Add definitions and lemmas for oriented angles defined to take an orientation, instead of an orthonormal basis, as an argument. These are the versions intended to be used by most users when working with oriented angles between vectors, instead of users needing to deal with a choice of basis. Apart from the last five lemmas that relate angles and rotations for different orientations or relate them explicitly to the definitions with respect to a basis, everything is deduced directly from the corresponding lemma that takes an orthonormal basis as an argument.