cos_eq — Mathlib

English

Let z be a complex number. Then cos z = cos(Re z) cosh(Im z) − i sin(Re z) sinh(Im z).

Русский

Пусть z является комплексным числом. Тогда cos z = cos(Re z) cosh(Im z) − i sin(Re z) sinh(Im z).

LaTeX

$$$ \cos z = \cos(\\operatorname{Re} z) \cosh(\\operatorname{Im} z) - i \\sin(\\operatorname{Re} z) \\sinh(\\operatorname{Im} z).$$$

Lean4

theorem cos_eq (z : ℂ) : cos z = cos z.re * cosh z.im - sin z.re * sinh z.im * I := by convert cos_add_mul_I z.re z.im;
  exact (re_add_im z).symm

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