tan_sq_div_one_add_tan_sq

Mathlib.Analysis.Complex.Trigonometric

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

← MathLib Explorer

English

cos(3x) = 4 cos^3 x − 3 cos x.

Русский

cos(3x) = 4 cos^3 x − 3 cos x.

LaTeX

$$$\\forall x \\in \\mathbb{C},\\; \\cos(3x) = 4\\cos^3 x - 3\\cos x$$$

Lean4

theorem tan_sq_div_one_add_tan_sq {x : ℂ} (hx : cos x ≠ 0) : tan x ^ 2 / (1 + tan x ^ 2) = sin x ^ 2 := by
  simp only [← tan_mul_cos hx, mul_pow, ← inv_one_add_tan_sq hx, div_eq_mul_inv]

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

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

Разделы

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

Аффилиация

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