cos_sub

Mathlib.Analysis.Complex.Trigonometric

URI: https://scilib.ai/kg/mathlib#Real.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