English
The real hyperbolic tangent is the real part of the complex hyperbolic tangent on real inputs; i.e., for x ∈ ℝ, Real.tanh x = Re( Complex.tanh( Complex.ofReal x ) ).
Русский
Гиперболический тангенс на вещественных входах равен вещественной части комплексного гиперболического тангенса: Real.tanh x = Re( Complex.tanh( Complex.ofReal x ) ).
LaTeX
$$$$ \operatorname{Real.tanh}(x) = \operatorname{Re}\bigl( \operatorname{tanh}(\operatorname{Complex.ofReal}(x)) \bigr). $$$$
Lean4
/-- The real hypebolic tangent function, defined as the real part of
the complex hyperbolic tangent -/
@[pp_nodot]
nonrec def tanh (x : ℝ) : ℝ :=
(tanh x).re
