mathlib

e8a45253 - feat(geometry/euclidean/angle/oriented/right_angle): trigonometric lemmas (#17683)

feat(geometry/euclidean/angle/oriented/right_angle): trigonometric lemmas (#17683) Add lemmas about trigonometric functions in relation to right-angled triangles with oriented angles. These are generally analogous to the unoriented case, but note that the property of an angle being a right angle is not symmetric with respect to reversing the order of the vectors / points in the oriented case (a positive right angle becomes a negative right angle). Thus, one unoriented lemma tends to correspond to two lemmas in the oriented case, in order to state the trigonometric results for both angles other than the right angle, since those results are no longer so trivially equivalent.