mathlib3

474f96ac - feat(geometry/euclidean/oriented_angle): more on relation to unoriented angles (#16215)

feat(geometry/euclidean/oriented_angle): more on relation to unoriented angles (#16215) Add more lemmas about the relation of oriented and unoriented angles; in particular, some involving `real.angle.to_real` and `real.angle.sign`.