mathlib

50f092eb - feat(analysis/special_functions/trigonometric/angle): signs of angles (#15967)

feat(analysis/special_functions/trigonometric/angle): signs of angles (#15967) Add a definition of `real.angle.sign` and some associated basic lemmas. This is intended for use in relating oriented and unoriented angles in Euclidean geometry (if the signs of two oriented angles between nonzero vectors are equal, then those angles are equal if and only if the corresponding unoriented angles are equal, and lots of lemmas can be stated of the form "these two angles have the same sign" or "these two angles have opposite signs").