Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-22 20:33 fa6e0243

View on Github →

feat(analysis/special_functions/trigonometric/angle): to_real (#16007) Define real.angle.to_real, converting a real.angle to a real in the interval Ioc (-π) π (the same interval used by complex.arg), and prove some associated lemmas. This is the inverse operation to coercing the result of complex.arg to real.angle, and is also useful for converting between oriented and unoriented angles.

Estimated changes

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

added theorem real.angle.abs_to_real_coe_eq_self_iff

added theorem real.angle.abs_to_real_le_pi

added theorem real.angle.abs_to_real_neg_coe_eq_self_iff

added theorem real.angle.coe_abs_to_real_of_sign_nonneg

added theorem real.angle.coe_to_Ico_mod

added theorem real.angle.coe_to_Ioc_mod

added theorem real.angle.coe_to_real

added theorem real.angle.cos_to_real

added theorem real.angle.eq_iff_abs_to_real_eq_of_sign_eq

added theorem real.angle.eq_iff_sign_eq_and_abs_to_real_eq

added theorem real.angle.neg_coe_abs_to_real_of_sign_nonpos

added theorem real.angle.neg_pi_lt_to_real

added theorem real.angle.sign_to_real

added theorem real.angle.sin_to_real

added theorem real.angle.to_Ioc_mod_to_real

added def real.angle.to_real

added theorem real.angle.to_real_coe

added theorem real.angle.to_real_coe_eq_self_iff

added theorem real.angle.to_real_coe_eq_self_iff_mem_Ioc

added theorem real.angle.to_real_eq_pi_iff

added theorem real.angle.to_real_eq_zero_iff

added theorem real.angle.to_real_inj

added theorem real.angle.to_real_injective

added theorem real.angle.to_real_le_pi

added theorem real.angle.to_real_mem_Ioc

added theorem real.angle.to_real_neg_iff_sign_neg

added theorem real.angle.to_real_nonneg_iff_sign_nonneg

added theorem real.angle.to_real_pi

added theorem real.angle.to_real_zero