circleMap_eq_center_iff

Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

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

English

circleMap c R θ equals the center c if and only if R = 0.

Русский

circleMap c R θ равно центру c тогда и только тогда, когда R = 0.

LaTeX

$$$ circleMap c R θ = c \iff R = 0 $$$

Lean4

@[simp]
theorem circleMap_eq_center_iff {c : ℂ} {R : ℝ} {θ : ℝ} : circleMap c R θ = c ↔ R = 0 := by
  simp [circleMap, Complex.exp_ne_zero]

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

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

Разделы

Аффилиация

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