exp_arg

Mathlib.Analysis.SpecialFunctions.Complex.Circle

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

English

For any z on the unit circle, exp(arg z) = z.

Русский

Для любого z на единичной окружности имеет место exp(arg z) = z.

LaTeX

$$$$\\forall z \\in \\text{Circle}: \\ \\exp(\\arg z) = z.$$$$

Lean4

@[simp]
theorem exp_arg (z : Circle) : exp (arg z) = z :=
  injective_arg <| arg_exp (neg_pi_lt_arg _) (arg_le_pi _)

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

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

Разделы

Аффилиация

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