mathlib3

77314cca - feat(analysis/special_functions/trigonometric/angle): twice angles adding to `π` (#17822)

feat(analysis/special_functions/trigonometric/angle): twice angles adding to `π` (#17822) Add lemmas that, if twice two angles add to `π`, the absolute value of the cosine of one equals the absolute value of the sine of the other.