Prove2Me

Derivative_of_Cosecant_Function

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

calculusderivativesproofwikitrigonometry

d/dx(csc x) = -cos(x)/sin^2(x) = -csc(x)*cot(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_Cosecant_Function (x : ℝ) (hx : Real.sin x ≠ 0) : deriv (fun t => 1 / Real.sin t) x = -(Real.cos x / Real.sin x ^ 2) := by sorry
Source
https://proofwiki.org/wiki/Derivative_of_Cosecant_Function

View graph