mathlib

e6210004 - feat(analysis/special_functions/trigonometric/angle): adding and subtracting `π / 2` (#17396)

feat(analysis/special_functions/trigonometric/angle): adding and subtracting `π / 2` (#17396) Add a series of lemmas about `real.angle.sin` and `real.angle.cos` for angles given by an addition or subtraction involving `π / 2`, all trivially deduced from the corresponding `real.sin` and `real.cos` lemmas.