cos_two_mul

Mathlib.Analysis.Complex.Trigonometric

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

← MathLib Explorer

English

For any complex x, sin(2x) = 2 sin x cos x.

Русский

Для любого комплексного x: sin(2x) = 2 sin x cos x.

LaTeX

$$$\\forall x \\in \\mathbb{C},\\; \\sin(2x) = 2 \\sin x \\cos x$$$

Lean4

theorem cos_two_mul : cos (2 * x) = 2 * cos x ^ 2 - 1 := by
  rw [cos_two_mul', eq_sub_iff_add_eq.2 (sin_sq_add_cos_sq x), ← sub_add, sub_add_eq_add_sub, two_mul]

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

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

Разделы

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

Аффилиация

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