hasDerivAt_tan

Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

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

← MathLib Explorer

English

Under the assumption cos x ≠ 0, the derivative of tan at x is 1/cos^2 x.

Русский

При условии cos x ≠ 0 производная тангенса в x равна 1/cos^2 x.

LaTeX

$$$ \text{If } \cos x \neq 0, \\quad \dfrac{d}{dx} \tan x = \dfrac{1}{\cos^2 x}. $$$

Lean4

theorem hasDerivAt_tan {x : ℝ} (h : cos x ≠ 0) : HasDerivAt tan (1 / cos x ^ 2) x :=
  mod_cast (Complex.hasDerivAt_tan (by exact mod_cast h)).real_of_complex

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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