Commit 2023-06-06 18:26 a30980e4

View on Github →

feat: port Analysis.SpecialFunctions.Trigonometric.Complex (#4744)

Estimated changes

Modified Mathlib.lean

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

added theorem Complex.continuousOn_tan

added theorem Complex.continuous_tan

added theorem Complex.cos_eq_cos_iff

added theorem Complex.cos_eq_iff_quadratic

added theorem Complex.cos_eq_zero_iff

added theorem Complex.cos_ne_zero_iff

added theorem Complex.cos_surjective

added theorem Complex.range_cos

added theorem Complex.range_sin

added theorem Complex.sin_eq_sin_iff

added theorem Complex.sin_eq_zero_iff

added theorem Complex.sin_ne_zero_iff

added theorem Complex.sin_surjective

added theorem Complex.tan_add'

added theorem Complex.tan_add

added theorem Complex.tan_add_mul_I

added theorem Complex.tan_eq

added theorem Complex.tan_eq_zero_iff

added theorem Complex.tan_int_mul_pi_div_two

added theorem Complex.tan_ne_zero_iff

added theorem Complex.tan_two_mul

added theorem Real.cos_eq_cos_iff

added theorem Real.cos_eq_zero_iff

added theorem Real.cos_ne_zero_iff

added theorem Real.le_sin_mul

added theorem Real.lt_sin_mul

added theorem Real.mul_le_sin

added theorem Real.mul_lt_sin

added theorem Real.sin_eq_sin_iff