Derivative_of_Secant_Function

Proved

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

calculusderivativesproofwikitrigonometry

d/dx(sec x) = sin(x)/cos^2(x) = sec(x)*tan(x) when cos(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_Secant_Function (x : ℝ) (hx : Real.cos x ≠ 0) : deriv (fun t => 1 / Real.cos t) x = Real.sin x / Real.cos x ^ 2 := by sorry

Source

https://proofwiki.org/wiki/Derivative_of_Secant_Function

View graph