Gamma_ne_zero_of_re_pos

Mathlib.Analysis.SpecialFunctions.Gamma.Beta

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

← MathLib Explorer

English

If Re(s) > 0 then Gamma(s) ≠ 0.

Русский

Если Re(s) > 0, тогда Gamma(s) ≠ 0.

LaTeX

$$$$ \Re(s) > 0 \implies \Gamma(s) \neq 0. $$$$

Lean4

/-- A weaker, but easier-to-apply, version of `Complex.Gamma_ne_zero`. -/
theorem Gamma_ne_zero_of_re_pos {s : ℂ} (hs : 0 < re s) : Gamma s ≠ 0 :=
  by
  refine Gamma_ne_zero fun m => ?_
  contrapose! hs
  simpa only [hs, neg_re, ← ofReal_natCast, ofReal_re, neg_nonpos] using Nat.cast_nonneg _

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

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

Разделы

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

Аффилиация

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