mathlib

674505ed - feat(geometry/euclidean/oriented_angle): relation to unoriented angles (#15722)

feat(geometry/euclidean/oriented_angle): relation to unoriented angles (#15722) Add some versions of the result that an oriented angle is plus or minus the unoriented angle between the same two vectors. There will be a lot more lemmas to add subsequently in this area (including, in particular, lemmas about when two angles have the same or different signs, that are needed to go from equality of unoriented angles to equality of oriented angles). This just provides the starting point for adding such results.