hasDerivAt_tan

Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv

URI: https://scilib.ai/kg/mathlib#Complex.hasDerivAt_tan

English

If cos x ≠ 0, then tan has derivative at x equal to 1/cos(x)^2.

Русский

Если cos x ≠ 0, то тангенс имеет производную в точке x равную 1/cos(x)^2.

LaTeX

$$$$ \text{HasDerivAt}(\tan, 1/\cos^2 x, x) \quad \text{if } \cos x \neq 0. $$$$

Lean4

theorem hasDerivAt_tan {x : ℂ} (h : cos x ≠ 0) : HasDerivAt tan (1 / cos x ^ 2) x :=
  (hasStrictDerivAt_tan h).hasDerivAt

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru