cos_sub

Mathlib.Analysis.Complex.Trigonometric

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

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_sub : cos (x - y) = cos x * cos y + sin x * sin y := by simp [sub_eq_add_neg, cos_add, sin_neg, cos_neg]

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

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

Разделы

Аффилиация

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