ofReal_tan

Mathlib.Analysis.Complex.Trigonometric

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

English

For real x, the complex value Real.tan x equals tan(Complex.ofReal x).

Русский

Для действительного x вещественное tan x равняется tan(Complex.ofReal x) в комплексном числе.

LaTeX

$$$ (\operatorname{Real.tan} x) : \mathbb{C} = \tan(\operatorname{Complex.ofReal} x).$$$

Lean4

@[simp, norm_cast]
theorem ofReal_tan (x : ℝ) : (Real.tan x : ℂ) = tan x :=
  ofReal_tan_ofReal_re _

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

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

Разделы

Аффилиация

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