tanh_mul_I

Mathlib.Analysis.Complex.Trigonometric

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

English

tanh(x I) = tan x · I.

Русский

tanh(x I) = tan x · I.

LaTeX

$$$\\tanh(x \\cdot \\mathrm{I}) = \\tan x \\cdot \\mathrm{I}$$$

Lean4

theorem tanh_mul_I : tanh (x * I) = tan x * I := by
  rw [tanh_eq_sinh_div_cosh, cosh_mul_I, sinh_mul_I, mul_div_right_comm, tan]

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

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

Разделы

Аффилиация

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