Commit 2026-09-30 15:24 4e720198
View on Github →feat(Geometry/Euclidean): unoriented angle eq of oriented angle eq (#40498)
This PR adds two theorems to Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
angle_eq_of_oangle_eq: If two oriented angles are equal, and the four endpoint pairs are nondegenerate, then the
corresponding unoriented angles are equal.
angle_eq_of_oangle_eq_not_collinear: If two oriented angles are equal, and the first triple is not collinear, then the
corresponding unoriented angles are equal.