mathlib

f1a2caaf - feat(analysis/special_functions/trigonometric/angle): `to_real` lemmas (#17395)

feat(analysis/special_functions/trigonometric/angle): `to_real` lemmas (#17395) Add a series of lemmas mainly about `real.angle.to_real` and twice angles, concluding with conditions for an angle and twice that angle to have the same sign (which is of use for proving that the base angles of an isosceles triangle are acute).