cos_add_mul_I

Mathlib.Analysis.Complex.Trigonometric

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

English

cos(x + y I) = cos x cosh y − sin x sinh y I.

Русский

cos(x + y I) = cos x cosh y − sin x sinh y I.

LaTeX

$$$\\cos(x + y \\cdot i) = \\cos x \\cosh y - \\sin x \\sinh y \\cdot i$$$

Lean4

theorem cos_add_mul_I (x y : ℂ) : cos (x + y * I) = cos x * cosh y - sin x * sinh y * I := by
  rw [cos_add, cos_mul_I, sin_mul_I, mul_assoc]

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

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

Разделы

Аффилиация

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