circleMap_zero_inv

Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

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

English

The inverse of circleMap 0 R θ is circleMap 0 R^{−1} (−θ).

Русский

Обратное отображение circleMap 0 R θ равно circleMap 0 R^{−1} (−θ).

LaTeX

$$$ (circleMap 0 R θ)^{-1} = circleMap 0 R^{-1} (-\theta) $$$

Lean4

theorem circleMap_zero_inv (R θ : ℝ) : (circleMap 0 R θ)⁻¹ = circleMap 0 R⁻¹ (-θ) := by
  simp [circleMap_zero, Complex.exp_neg, mul_comm]

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

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

Разделы

Аффилиация

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