sin_sub

Mathlib.Analysis.Complex.Trigonometric

URI: https://scilib.ai/kg/mathlib#Real.sin_sub

English

For all real x,y, sin(x - y) = sin x cos y - cos x sin y.

Русский

Для любых x,y ∈ ℝ: sin(x−y) = sin x cos y − cos x sin y.

LaTeX

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

Lean4

theorem sin_sub : sin (x - y) = sin x * cos y - cos x * sin y := by simp [sub_eq_add_neg, sin_add, sin_neg, cos_neg]

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

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

Разделы

Аффилиация

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