deriv_tan — Mathlib

English

The derivative of tan is 1/(cos x)^2; at points where cos x = 0, tan is not differentiable.

Русский

Производная тангенса равна 1/ cos^2 x; в точках, где cos x = 0, тангенс не дифференцируем.

LaTeX

$$$$\text{deriv}(\tan x) = \frac{1}{\cos^2 x} \quad\text{whenever } \cos x \neq 0.$$$$

Lean4

@[simp]
theorem deriv_tan (x : ℂ) : deriv tan x = 1 / cos x ^ 2 :=
  if h : cos x = 0 then
    by
    have : ¬DifferentiableAt ℂ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h)
    simp [deriv_zero_of_not_differentiableAt this, h, sq]
  else (hasDerivAt_tan h).deriv

Похожие утверждения