Commit 2023-06-06 20:03 02219c18

View on Github →

feat: port Analysis.SpecialFunctions.Trigonometric.ComplexDeriv (#4753)

Estimated changes

Modified Mathlib.lean

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

added theorem Complex.contDiffAt_tan

added theorem Complex.continuousAt_tan

added theorem Complex.deriv_tan

added theorem Complex.differentiableAt_tan

added theorem Complex.hasDerivAt_tan

added theorem Complex.hasStrictDerivAt_tan

added theorem Complex.tendsto_abs_tan_atTop

added theorem Complex.tendsto_abs_tan_of_cos_eq_zero