Theorem AnalyticOnNhd.re_ofReal

Modification history

2025-01-29 06:49

Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean

feat: the moment generating function is analytic (#20151) …

Added AnalyticOnNhd.re_ofReal View on Github →