qParam_ne_zero

Mathlib.Analysis.Complex.Periodic

URI: https://scilib.ai/kg/mathlib#Function.Periodic.qParam_ne_zero

English

Let h be a real number. For every z in the complex plane, the value qParam(h, z) is never zero.

Русский

Пусть h — действительное число. Для любого z ∈ ℂ значение qParam(h, z) никогда не равно нулю.

LaTeX

$$$\forall z \in \mathbb{C},\; qParam(h,z) \neq 0$$$

Lean4

theorem qParam_ne_zero (z : ℂ) : 𝕢 h z ≠ 0 := by simp [qParam, exp_ne_zero]

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

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

Разделы

Аффилиация

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