neg_pi_lt_log_im

Mathlib.Analysis.SpecialFunctions.Complex.Log

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

English

The imaginary part of log x is strictly greater than -π: -π < Im(log x).

Русский

Воображаемая часть log x строго больше -π: -π < Im(log x).

LaTeX

$$$-\pi < \operatorname{Im}(\log x).$$$

Lean4

theorem neg_pi_lt_log_im (x : ℂ) : -π < (log x).im := by simp only [log_im, neg_pi_lt_arg]

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

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

Разделы

Аффилиация

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