circleMap_pi_div_two

Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

URI: https://scilib.ai/kg/mathlib#circleMap_pi_div_two

← MathLib Explorer

English

CircleMap at angle π/2 yields the imaginary increment: circleMap c R (π/2) = c + R i.

Русский

Значение при угле π/2 даёт мнимую составляющую: circleMap c R (π/2) = c + R i.

LaTeX

$$$ circleMap c R (\tfrac{\pi}{2}) = c + R i $$$

Lean4

theorem circleMap_pi_div_two (c : ℂ) (R : ℝ) : circleMap c R (π / 2) = c + R * I := by
  simp only [circleMap, ofReal_div, ofReal_ofNat, exp_pi_div_two_mul_I]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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