circleMap_zero

Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

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

English

When the center is 0, circleMap(0,R,θ) reduces to R e^{i θ}.

Русский

Если центр равен нулю, то circleMap 0 R θ = R e^{i θ}.

LaTeX

$$$ circleMap 0 R θ = R e^{i \theta} $$$

Lean4

theorem circleMap_zero (R θ : ℝ) : circleMap 0 R θ = R * exp (θ * I) :=
  zero_add _

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

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

Разделы

Аффилиация

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