two_pi_I_ne_zero

Mathlib.Analysis.SpecialFunctions.Complex.Log

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

English

The complex number 2πi is nonzero.

Русский

Комплексное число 2πi не равно нулю.

LaTeX

$$$2\pi i \neq 0$$$

Lean4

theorem two_pi_I_ne_zero : (2 * π * I : ℂ) ≠ 0 := by simp [Real.pi_ne_zero, I_ne_zero]

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

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

Разделы

Аффилиация

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