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).

Estimated changes

Modified src/analysis/special_functions/trigonometric/angle.lean

added theorem real.angle.nsmul_to_real_eq_mul

added theorem real.angle.sign_two_nsmul_eq_sign_iff

added theorem real.angle.sign_two_zsmul_eq_sign_iff

added theorem real.angle.to_real_coe_eq_self_add_two_pi_iff

added theorem real.angle.to_real_coe_eq_self_sub_two_mul_int_mul_pi_iff

added theorem real.angle.to_real_coe_eq_self_sub_two_pi_iff

added theorem real.angle.two_nsmul_coe_div_two

added theorem real.angle.two_nsmul_neg_pi_div_two

added theorem real.angle.two_nsmul_to_real_eq_two_mul

added theorem real.angle.two_nsmul_to_real_eq_two_mul_add_two_pi

added theorem real.angle.two_nsmul_to_real_eq_two_mul_sub_two_pi

added theorem real.angle.two_zsmul_coe_div_two

added theorem real.angle.two_zsmul_neg_pi_div_two

added theorem real.angle.two_zsmul_to_real_eq_two_mul

added theorem real.angle.two_zsmul_to_real_eq_two_mul_add_two_pi

added theorem real.angle.two_zsmul_to_real_eq_two_mul_sub_two_pi