toCircle_coe

Mathlib.Analysis.SpecialFunctions.Complex.Circle

URI: https://scilib.ai/kg/mathlib#Real.Angle.toCircle_coe

English

For any real x, the image toCircle x equals exp x.

Русский

Для любого действительного x отображение toCircle x равно exp x.

LaTeX

$$$$ toCircle(x) = \exp(x). $$$$

Lean4

@[simp]
theorem toCircle_coe (x : ℝ) : toCircle x = .exp x :=
  rfl

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

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

Разделы

Аффилиация

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