mathlib3

1534854c - feat(geometry/euclidean/angle/oriented/affine): `π / 2` lemmas (#17487)

feat(geometry/euclidean/angle/oriented/affine): `π / 2` lemmas (#17487) Add a series of lemmas relating an oriented angle of `π / 2` or `-π / 2` between three points to the unoriented angle being `π / 2`.