arg_exp

Mathlib.Analysis.SpecialFunctions.Complex.Circle

URI: https://scilib.ai/kg/mathlib#Circle.arg_exp

English

For real x with -π < x ≤ π, arg(e^x) = x.

Русский

Для вещественного x, удовлетворяющего -π < x ≤ π, имеет место arg(e^x) = x.

LaTeX

$$$$\\forall x\\in\\mathbb{R},\\ -\\pi < x \\le \\pi \\Rightarrow \\arg (\\exp x) = x.$$$$

Lean4

theorem arg_exp {x : ℝ} (h₁ : -π < x) (h₂ : x ≤ π) : arg (exp x) = x := by
  rw [coe_exp, exp_mul_I, arg_cos_add_sin_mul_I ⟨h₁, h₂⟩]

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

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

Разделы

Аффилиация

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