cos_add

Mathlib.Analysis.Complex.Trigonometric

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

← MathLib Explorer

English

cos(x+y) = cos x cos y − sin x sin y.

Русский

cos(x+y) = cos x cos y − sin x sin y.

LaTeX

$$$\\cos(x+y) = \\cos x \\cos y - \\sin x \\sin y$$$

Lean4

theorem cos_add : cos (x + y) = cos x * cos y - sin x * sin y := by
  rw [← cosh_mul_I, add_mul, cosh_add, cosh_mul_I, cosh_mul_I, sinh_mul_I, sinh_mul_I, mul_mul_mul_comm, I_mul_I,
    mul_neg_one, sub_eq_add_neg]

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

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

Разделы

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

Аффилиация

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