Commit 2023-06-07 00:58 04a303a3

View on Github →

feat: port Analysis.SpecialFunctions.Trigonometric.ArctanDeriv (#4764)

Estimated changes

Modified Mathlib.lean

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

added theorem ContDiff.arctan

added theorem ContDiffAt.arctan

added theorem ContDiffOn.arctan

added theorem ContDiffWithinAt.arctan

added theorem Differentiable.arctan

added theorem DifferentiableAt.arctan

added theorem DifferentiableOn.arctan

added theorem DifferentiableWithinAt.arctan

added theorem HasDerivAt.arctan

added theorem HasDerivWithinAt.arctan

added theorem HasFDerivAt.arctan

added theorem HasFDerivWithinAt.arctan

added theorem HasStrictDerivAt.arctan

added theorem HasStrictFDerivAt.arctan

added theorem Real.contDiffAt_tan

added theorem Real.contDiff_arctan

added theorem Real.continuousAt_tan

added theorem Real.deriv_arctan

added theorem Real.deriv_tan

added theorem Real.differentiableAt_arctan

added theorem Real.differentiableAt_tan

added theorem Real.differentiableAt_tan_of_mem_Ioo

added theorem Real.differentiable_arctan

added theorem Real.hasDerivAt_arctan

added theorem Real.hasDerivAt_tan

added theorem Real.hasDerivAt_tan_of_mem_Ioo

added theorem Real.hasStrictDerivAt_arctan

added theorem Real.hasStrictDerivAt_tan

added theorem Real.tendsto_abs_tan_atTop

added theorem Real.tendsto_abs_tan_of_cos_eq_zero

added theorem derivWithin_arctan

added theorem deriv_arctan

added theorem fderivWithin_arctan

added theorem fderiv_arctan