mathlib

f8393c90 - feat(analysis/special_functions/trigonometric/angle): sign and π / 2 lemmas (#17129)

feat(analysis/special_functions/trigonometric/angle): sign and π / 2 lemmas (#17129) Add various lemmas about signs of `real.angle` and right angles as a `real.angle`. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>