Commit 2023-05-18 04:09 5a1d44af

View on Github →

feat: port Analysis.SpecialFunctions.Complex.Arg (#4041)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean

added theorem Complex.abs_arg_le_pi

added theorem Complex.abs_arg_le_pi_div_two_iff

added theorem Complex.abs_eq_one_iff

added theorem Complex.abs_mul_cos_add_sin_mul_I

added theorem Complex.abs_mul_exp_arg_mul_I

added theorem Complex.arg_I

added theorem Complex.arg_coe_angle_eq_iff

added theorem Complex.arg_coe_angle_eq_iff_eq_toReal

added theorem Complex.arg_coe_angle_toReal_eq_arg

added theorem Complex.arg_conj

added theorem Complex.arg_conj_coe_angle

added theorem Complex.arg_cos_add_sin_mul_I

added theorem Complex.arg_cos_add_sin_mul_I_coe_angle

added theorem Complex.arg_cos_add_sin_mul_I_eq_toIocMod

added theorem Complex.arg_cos_add_sin_mul_I_sub

added theorem Complex.arg_div_coe_angle

added theorem Complex.arg_eq_arg_iff

added theorem Complex.arg_eq_neg_pi_div_two_iff

added theorem Complex.arg_eq_nhds_of_im_neg

added theorem Complex.arg_eq_nhds_of_im_pos

added theorem Complex.arg_eq_nhds_of_re_neg_of_im_neg

added theorem Complex.arg_eq_nhds_of_re_neg_of_im_pos

added theorem Complex.arg_eq_nhds_of_re_pos

added theorem Complex.arg_eq_pi_div_two_iff

added theorem Complex.arg_eq_pi_iff

added theorem Complex.arg_eq_zero_iff

added theorem Complex.arg_inv

added theorem Complex.arg_inv_coe_angle

added theorem Complex.arg_le_pi

added theorem Complex.arg_le_pi_div_two_iff

added theorem Complex.arg_lt_pi_iff

added theorem Complex.arg_mem_Ioc

added theorem Complex.arg_mul_coe_angle

added theorem Complex.arg_mul_cos_add_sin_mul_I

added theorem Complex.arg_mul_cos_add_sin_mul_I_coe_angle

added theorem Complex.arg_mul_cos_add_sin_mul_I_eq_toIocMod

added theorem Complex.arg_mul_cos_add_sin_mul_I_sub

added theorem Complex.arg_neg_I

added theorem Complex.arg_neg_coe_angle

added theorem Complex.arg_neg_eq_arg_add_pi_iff

added theorem Complex.arg_neg_eq_arg_add_pi_of_im_neg

added theorem Complex.arg_neg_eq_arg_sub_pi_iff

added theorem Complex.arg_neg_eq_arg_sub_pi_of_im_pos

added theorem Complex.arg_neg_iff

added theorem Complex.arg_neg_one

added theorem Complex.arg_nonneg_iff

added theorem Complex.arg_of_im_neg

added theorem Complex.arg_of_im_nonneg_of_ne_zero

added theorem Complex.arg_of_im_pos

added theorem Complex.arg_of_re_neg_of_im_neg

added theorem Complex.arg_of_re_neg_of_im_nonneg

added theorem Complex.arg_of_re_nonneg

added theorem Complex.arg_of_real_of_neg

added theorem Complex.arg_of_real_of_nonneg

added theorem Complex.arg_one

added theorem Complex.arg_real_mul

added theorem Complex.arg_zero

added theorem Complex.continuousAt_arg

added theorem Complex.continuousAt_arg_coe_angle

added theorem Complex.continuousWithinAt_arg_of_re_neg_of_im_zero

added theorem Complex.cos_arg

added theorem Complex.ext_abs_arg

added theorem Complex.ext_abs_arg_iff

added theorem Complex.neg_pi_div_two_le_arg_iff

added theorem Complex.neg_pi_lt_arg

added theorem Complex.range_arg

added theorem Complex.range_exp_mul_I

added theorem Complex.sin_arg

added theorem Complex.tan_arg

added theorem Complex.tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero

added theorem Complex.tendsto_arg_nhdsWithin_im_nonneg_of_re_neg_of_im_zero