Gammaℝ_ne_zero_of_re_pos

Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

URI: https://scilib.ai/kg/mathlib#Complex.Gammaℝ_ne_zero_of_re_pos

← MathLib Explorer

English

If Re(s) > 0, then Γℝ(s) ≠ 0.

Русский

Если Re(s) > 0, то Γℝ(s) ≠ 0.

LaTeX

$$$ \Re(s) > 0 \implies \Gamma\mathbb{R}(s) \neq 0 $$$

Lean4

theorem Gammaℝ_ne_zero_of_re_pos {s : ℂ} (hs : 0 < re s) : Gammaℝ s ≠ 0 :=
  by
  apply mul_ne_zero
  · simp [pi_ne_zero]
  · apply Gamma_ne_zero_of_re_pos
    rw [div_ofNat_re]
    exact div_pos hs two_pos

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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