deriv_tan — Mathlib

English

The derivative of arctan at x is 1/(1+x^2) for all x.

Русский

Производная арктангенса в точке x равна 1/(1+x^2) для всех x.

LaTeX

$$$ \frac{d}{dx} \arctan x = \frac{1}{1+x^2}. $$$

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

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