eulerMascheroniConstant_eq_neg_deriv

English

Euler–Mascheroni constant γ equals the negative of the derivative of Gamma at 1: γ = −deriv Γ(1).

Русский

Константа Эйлера–Машчерони γ равна минус производная гаммы в точке 1: γ = −deriv Γ(1).

LaTeX

$$\gamma = -\operatorname{deriv} \Gamma (1)$$

Lean4

theorem eulerMascheroniConstant_eq_neg_deriv : γ = -deriv Gamma 1 :=
  by
  rw [show (1 : ℝ) = ↑(0 : ℕ) + 1 by simp, deriv_Gamma_nat 0]
  simp

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