sin_eq

Mathlib.Analysis.Complex.Trigonometric

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

English

For every complex z, sin z = sin(Re z) cosh(Im z) + cos(Re z) sinh(Im z) I.

Русский

Для каждого комплексного z верно sin z = sin(Re z) cosh(Im z) + cos(Re z) sinh(Im z) i.

LaTeX

$$$\\sin z = \\sin(\\Re z) \\cosh(\\Im z) + \\cos(\\Re z) \\sinh(\\Im z) \\cdot i$$$

Lean4

theorem sin_eq (z : ℂ) : sin z = sin z.re * cosh z.im + cos z.re * sinh z.im * I := by convert sin_add_mul_I z.re z.im;
  exact (re_add_im z).symm

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

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

Разделы

Аффилиация

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