Commit 2025-11-04 20:03 8c6c6262
View on Github →feat(Analysis/SpecialFunctions/Trigonometric/Angle): angles adding to 0 mod π (#30943)
Add lemmas that if two angles with the same nonzero sign add to 0 mod π, then the absolute values of the corresponding real numbers obtained with toReal (unoriented angles) add to π.