tan — Mathlib

English

The real tangent is the real part of the complex tangent on real inputs; i.e., for x ∈ ℝ, Real.tan x = Re( Complex.tan( Complex.ofReal x ) ).

Русский

Реальный тангенс является вещественной частью комплексного тангенса на вещественных входах: для x ∈ ℝ Real.tan x = Re( Complex.tan( Complex.ofReal x ) ).

LaTeX

$$$$ \operatorname{Real.tan}(x) = \operatorname{Re}\bigl( \operatorname{tan}(\operatorname{Complex.ofReal}(x)) \bigr). $$$$

Lean4

/-- The real tangent function, defined as the real part of the complex tangent -/
@[pp_nodot]
nonrec def tan (x : ℝ) : ℝ :=
  (tan x).re

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