slitPlane_arg_ne_pi

Mathlib.Analysis.SpecialFunctions.Complex.Arg

URI: https://scilib.ai/kg/mathlib#Complex.slitPlane_arg_ne_pi

English

If z is in the slit plane, then z.arg ≠ π.

Русский

Если z принадлежит слитной плоскости, то z.arg ≠ π.

LaTeX

$$$ z \in \text{slitPlane} \;\Rightarrow\; z.arg \neq \pi $$$

Lean4

theorem slitPlane_arg_ne_pi {z : ℂ} (hz : z ∈ slitPlane) : z.arg ≠ Real.pi :=
  (mem_slitPlane_iff_arg.mp hz).1

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

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

Разделы

Аффилиация

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