tanh_conj

Mathlib.Analysis.Complex.Trigonometric

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

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

theorem tanh_conj : tanh (conj x) = conj (tanh x) := by rw [tanh, sinh_conj, cosh_conj, ← map_div₀, tanh]

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

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

Разделы

Аффилиация

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