Commit 2022-02-21 15:30 95d22b52

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 π).