ofReal_cos

Mathlib.Analysis.Complex.Trigonometric

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

English

For real x, embedding Real.cos x into the complex plane equals cos x.

Русский

Для действительного x вложение Real.cos x в комплексное число равно cos x.

LaTeX

$$$ (\operatorname{Real.cos} x : \mathbb{C}) = \cos x.$$$

Lean4

@[simp, norm_cast]
theorem ofReal_cos (x : ℝ) : (Real.cos x : ℂ) = cos x :=
  ofReal_cos_ofReal_re _

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

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

Разделы

Аффилиация

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