mathlib3

ddc74844 - feat(geometry/euclidean/oriented_angle): signs of angles between linear combinations of vectors (#16243)

feat(geometry/euclidean/oriented_angle): signs of angles between linear combinations of vectors (#16243) Add a series of lemmas giving the sign of the oriented angle between two linear combinations of two vectors in terms of the sign of the angle between the original two vectors and the coefficients in the linear combination.