inv_one_add_tan_sq

Mathlib.Analysis.Complex.Trigonometric

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

← MathLib Explorer

English

cos x ≠ 0 → (1 + tan^2 x)^{-1} = cos^2 x

Русский

cos x ≠ 0 → (1 + tan^2 x)^{-1} = cos^2 x

LaTeX

$$\$\\cos x \\neq 0 \\Rightarrow (1 + \\tan^2 x)^{-1} = \\cos^2 x\$$$

Lean4

theorem inv_one_add_tan_sq {x : ℝ} (hx : cos x ≠ 0) : (1 + tan x ^ 2)⁻¹ = cos x ^ 2 :=
  have : Complex.cos x ≠ 0 := mt (congr_arg re) hx
  ofReal_inj.1 <| by simpa using Complex.inv_one_add_tan_sq this

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

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

Разделы

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

Аффилиация

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