cos

Mathlib.Analysis.Complex.Trigonometric

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

English

Let z be a complex number. The complex cosine function is defined by cos z = (e^{i z} + e^{-i z})/2.

Русский

Пусть z - комплексное число. Комплексная функция косинуса определяется как cos z = (e^{i z} + e^{-i z})/2.

LaTeX

$$$$ \cos z = \frac{e^{iz} + e^{-iz}}{2} $$$$

Lean4

/-- The complex cosine function, defined via `exp` -/
@[pp_nodot]
def cos (z : ℂ) : ℂ :=
  (exp (z * I) + exp (-z * I)) / 2

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

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

Разделы

Аффилиация

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