ofReal_tanh

Mathlib.Analysis.Complex.Trigonometric

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

English

Conjugation commutes with tanh: tanh(conj x) = conj(tanh x).

Русский

Сопряжение числа и tanh совпадает: tanh(conj x) = conj(tanh x).

LaTeX

$$$\tanh(\overline{x}) = \overline{\tanh x}$$$

Lean4

@[simp, norm_cast]
theorem ofReal_tanh (x : ℝ) : (Real.tanh x : ℂ) = tanh x :=
  ofReal_tanh_ofReal_re _

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

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

Разделы

Аффилиация

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