mathlib3

074ba985 - feat(geometry/euclidean/oriented_angle): oriented angles between points (#16279)

feat(geometry/euclidean/oriented_angle): oriented angles between points (#16279) Define the oriented angle between three points, notation `∡`, in terms of that between two vectors, and set up some corresponding basic API (including relating it to unoriented angles between three points). For angles between points, the choice of orientation is implicit, via use of the `module.oriented` typeclass to specify a preferred orientation.