Commit 2023-05-17 11:25 8886682a

View on Github →

feat: port Analysis.SpecialFunctions.Trigonometric.Angle (#4040)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean

added theorem ContinuousOn.angle_sign_comp

added theorem Real.Angle.abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi

added theorem Real.Angle.abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi

added theorem Real.Angle.abs_cos_eq_of_two_nsmul_eq

added theorem Real.Angle.abs_cos_eq_of_two_zsmul_eq

added theorem Real.Angle.abs_sin_eq_of_two_nsmul_eq

added theorem Real.Angle.abs_sin_eq_of_two_zsmul_eq

added theorem Real.Angle.abs_toReal_coe_eq_self_iff

added theorem Real.Angle.abs_toReal_eq_pi_div_two_iff

added theorem Real.Angle.abs_toReal_le_pi

added theorem Real.Angle.abs_toReal_neg_coe_eq_self_iff

added theorem Real.Angle.angle_eq_iff_two_pi_dvd_sub

added def Real.Angle.coeHom

added theorem Real.Angle.coe_abs_toReal_of_sign_nonneg

added theorem Real.Angle.coe_add

added theorem Real.Angle.coe_coeHom

added theorem Real.Angle.coe_int_mul_eq_zsmul

added theorem Real.Angle.coe_nat_mul_eq_nsmul

added theorem Real.Angle.coe_neg

added theorem Real.Angle.coe_nsmul

added theorem Real.Angle.coe_pi_add_coe_pi

added theorem Real.Angle.coe_sub

added theorem Real.Angle.coe_toIcoMod

added theorem Real.Angle.coe_toIocMod

added theorem Real.Angle.coe_toReal

added theorem Real.Angle.coe_two_pi

added theorem Real.Angle.coe_zero

added theorem Real.Angle.coe_zsmul

added theorem Real.Angle.continuousAt_sign

added theorem Real.Angle.continuous_coe

added theorem Real.Angle.continuous_cos

added theorem Real.Angle.continuous_sin

added def Real.Angle.cos

added theorem Real.Angle.cos_add

added theorem Real.Angle.cos_add_pi

added theorem Real.Angle.cos_add_pi_div_two

added theorem Real.Angle.cos_antiperiodic

added theorem Real.Angle.cos_coe

added theorem Real.Angle.cos_coe_pi

added theorem Real.Angle.cos_eq_iff_coe_eq_or_eq_neg

added theorem Real.Angle.cos_eq_iff_eq_or_eq_neg

added theorem Real.Angle.cos_eq_real_cos_iff_eq_or_eq_neg

added theorem Real.Angle.cos_eq_zero_iff

added theorem Real.Angle.cos_neg

added theorem Real.Angle.cos_neg_iff_pi_div_two_lt_abs_toReal

added theorem Real.Angle.cos_nonneg_iff_abs_toReal_le_pi_div_two

added theorem Real.Angle.cos_pi_div_two_sub

added theorem Real.Angle.cos_pos_iff_abs_toReal_lt_pi_div_two

added theorem Real.Angle.cos_sin_inj

added theorem Real.Angle.cos_sq_add_sin_sq

added theorem Real.Angle.cos_sub_pi

added theorem Real.Angle.cos_sub_pi_div_two

added theorem Real.Angle.cos_toReal

added theorem Real.Angle.cos_zero

added theorem Real.Angle.eq_iff_abs_toReal_eq_of_sign_eq

added theorem Real.Angle.eq_iff_sign_eq_and_abs_toReal_eq

added theorem Real.Angle.eq_neg_self_iff

added theorem Real.Angle.ne_neg_self_iff

added theorem Real.Angle.neg_coe_abs_toReal_of_sign_nonpos

added theorem Real.Angle.neg_coe_pi

added theorem Real.Angle.neg_eq_self_iff

added theorem Real.Angle.neg_ne_self_iff

added theorem Real.Angle.neg_pi_div_two_ne_zero

added theorem Real.Angle.neg_pi_lt_toReal

added theorem Real.Angle.nsmul_eq_iff

added theorem Real.Angle.nsmul_toReal_eq_mul

added theorem Real.Angle.pi_div_two_ne_zero

added theorem Real.Angle.pi_ne_zero

added def Real.Angle.sign

added theorem Real.Angle.sign_add_pi

added theorem Real.Angle.sign_antiperiodic

added theorem Real.Angle.sign_coe_neg_pi_div_two

added theorem Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi

added theorem Real.Angle.sign_coe_pi

added theorem Real.Angle.sign_coe_pi_div_two

added theorem Real.Angle.sign_eq_of_continuousOn

added theorem Real.Angle.sign_eq_zero_iff

added theorem Real.Angle.sign_ne_zero_iff

added theorem Real.Angle.sign_neg

added theorem Real.Angle.sign_neg_coe_nonpos_of_nonneg_of_le_pi

added theorem Real.Angle.sign_pi_add

added theorem Real.Angle.sign_pi_sub

added theorem Real.Angle.sign_sub_pi

added theorem Real.Angle.sign_toReal

added theorem Real.Angle.sign_two_nsmul_eq_sign_iff

added theorem Real.Angle.sign_two_zsmul_eq_sign_iff

added theorem Real.Angle.sign_zero

added def Real.Angle.sin

added theorem Real.Angle.sin_add

added theorem Real.Angle.sin_add_pi

added theorem Real.Angle.sin_add_pi_div_two

added theorem Real.Angle.sin_antiperiodic

added theorem Real.Angle.sin_coe

added theorem Real.Angle.sin_coe_pi

added theorem Real.Angle.sin_eq_iff_coe_eq_or_add_eq_pi

added theorem Real.Angle.sin_eq_iff_eq_or_add_eq_pi

added theorem Real.Angle.sin_eq_real_sin_iff_eq_or_add_eq_pi

added theorem Real.Angle.sin_eq_zero_iff

added theorem Real.Angle.sin_ne_zero_iff

added theorem Real.Angle.sin_neg

added theorem Real.Angle.sin_pi_div_two_sub

added theorem Real.Angle.sin_sub_pi

added theorem Real.Angle.sin_sub_pi_div_two

added theorem Real.Angle.sin_toReal

added theorem Real.Angle.sin_zero

added theorem Real.Angle.sub_coe_pi_eq_add_coe_pi

added def Real.Angle.tan

added theorem Real.Angle.tan_add_pi

added theorem Real.Angle.tan_coe

added theorem Real.Angle.tan_coe_pi

added theorem Real.Angle.tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi

added theorem Real.Angle.tan_eq_inv_of_two_zsmul_add_two_zsmul_eq_pi

added theorem Real.Angle.tan_eq_of_two_nsmul_eq

added theorem Real.Angle.tan_eq_of_two_zsmul_eq

added theorem Real.Angle.tan_eq_sin_div_cos

added theorem Real.Angle.tan_periodic

added theorem Real.Angle.tan_sub_pi

added theorem Real.Angle.tan_toReal

added theorem Real.Angle.tan_zero

added theorem Real.Angle.toIocMod_toReal

added def Real.Angle.toReal

added theorem Real.Angle.toReal_coe

added theorem Real.Angle.toReal_coe_eq_self_add_two_pi_iff

added theorem Real.Angle.toReal_coe_eq_self_iff

added theorem Real.Angle.toReal_coe_eq_self_iff_mem_Ioc

added theorem Real.Angle.toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff

added theorem Real.Angle.toReal_coe_eq_self_sub_two_pi_iff

added theorem Real.Angle.toReal_eq_neg_pi_div_two_iff

added theorem Real.Angle.toReal_eq_pi_div_two_iff

added theorem Real.Angle.toReal_eq_pi_iff

added theorem Real.Angle.toReal_eq_zero_iff

added theorem Real.Angle.toReal_inj

added theorem Real.Angle.toReal_injective

added theorem Real.Angle.toReal_le_pi

added theorem Real.Angle.toReal_mem_Ioc

added theorem Real.Angle.toReal_neg_iff_sign_neg

added theorem Real.Angle.toReal_neg_pi_div_two

added theorem Real.Angle.toReal_nonneg_iff_sign_nonneg

added theorem Real.Angle.toReal_pi

added theorem Real.Angle.toReal_pi_div_two

added theorem Real.Angle.toReal_zero

added theorem Real.Angle.two_nsmul_coe_div_two

added theorem Real.Angle.two_nsmul_coe_pi

added theorem Real.Angle.two_nsmul_eq_iff

added theorem Real.Angle.two_nsmul_eq_pi_iff

added theorem Real.Angle.two_nsmul_eq_zero_iff

added theorem Real.Angle.two_nsmul_ne_zero_iff

added theorem Real.Angle.two_nsmul_neg_pi_div_two

added theorem Real.Angle.two_nsmul_toReal_eq_two_mul

added theorem Real.Angle.two_nsmul_toReal_eq_two_mul_add_two_pi

added theorem Real.Angle.two_nsmul_toReal_eq_two_mul_sub_two_pi

added theorem Real.Angle.two_zsmul_coe_div_two

added theorem Real.Angle.two_zsmul_coe_pi

added theorem Real.Angle.two_zsmul_eq_iff

added theorem Real.Angle.two_zsmul_eq_pi_iff

added theorem Real.Angle.two_zsmul_eq_zero_iff

added theorem Real.Angle.two_zsmul_ne_zero_iff

added theorem Real.Angle.two_zsmul_neg_pi_div_two

added theorem Real.Angle.two_zsmul_toReal_eq_two_mul

added theorem Real.Angle.two_zsmul_toReal_eq_two_mul_add_two_pi

added theorem Real.Angle.two_zsmul_toReal_eq_two_mul_sub_two_pi

added theorem Real.Angle.zsmul_eq_iff

added def Real.Angle

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

added theorem Real.tan_pi