cos_add

Mathlib.Analysis.Complex.Trigonometric

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

English

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

Русский

Для любых x,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

nonrec theorem cos_add : cos (x + y) = cos x * cos y - sin x * sin y :=
  ofReal_injective <| by simp [cos_add]

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

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

Разделы

Аффилиация

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