Commit 2022-12-05 05:36 f1a2caaf
View on Github →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).