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.

Estimated changes