mathlib

da5e1327 - feat(geometry/euclidean/angle/oriented): nonzero angle lemmas (#17272)

feat(geometry/euclidean/angle/oriented): nonzero angle lemmas (#17272) Add a series of lemmas that, if the oriented angle between two vectors is nonzero, the vectors are nonzero and not equal to each other, and likewise for the most common specific nonzero values of the angle and for statements about its sign. Similarly, in the affine case, add such lemmas that any two of the three points in a nonzero angle are not equal.