ofReal_sin — Mathlib

English

The complex embedding of the real sine equals the complex sine: (Real.sin x : ℂ) = sin(Complex.ofReal x).

Русский

Комплексное вложение вещественной синусоиды равно комплексной синусе: (Real.sin x : ℂ) = sin(Complex.ofReal x).

LaTeX

$$$\mathrm{ofReal}(\sin x) = \sin(\mathrm{ofReal}(x))$$$

Lean4

@[simp, norm_cast]
theorem ofReal_sin (x : ℝ) : (Real.sin x : ℂ) = sin x :=
  ofReal_sin_ofReal_re _

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