mathlib

95d22b52 - feat(geometry/euclidean/oriented_angle): oriented angles and rotations (#12106)

feat(geometry/euclidean/oriented_angle): oriented angles and rotations (#12106) Define oriented angles and rotations in a real inner product space, with respect to a choice of orthonormal basis indexed by `fin 2`, and prove various lemmas about them, including that the definition depends only on the orientation associated with the basis, and geometrical results such as pons asinorum, "angle at center of a circle equals twice angle at circumference" and "angles in same segment are equal" / "opposite angles of a cyclic quadrilateral add to π" (these last two being the same result for oriented angles mod π).