mathlib

878c6289 - feat(geometry/euclidean/angle/oriented): more sign lemmas (#17270)

feat(geometry/euclidean/angle/oriented): more sign lemmas (#17270) Add more lemmas about signs of oriented angles: relation to unoriented angles when the sign is given as 1 or as -1, plus a series of (mostly `@[simp]`) lemmas for signs of angles between linear combinations of vectors, that follow readily from the existing lemmas for such combinations but avoid the need for manipulation using `one_smul` and similar at the site of use.