Derivative_of_Cotangent_Function
Provedcalculusderivativesproofwikitrigonometry
d/dx(cot x) = -1/sin^2(x) when sin(x) != 0.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv theorem Derivative_of_Cotangent_Function (x : ℝ) (hx : Real.sin x ≠ 0) : deriv (fun t => Real.cos t / Real.sin t) x = -(1 / Real.sin x ^ 2) := by sorry
Source