noncomputable def infiniteSumTerm (n : ℕ) : ℝ

Equations

• infiniteSumTerm n = 1 / ↑n - Real.log ((↑n + 1) / ↑n)

theorem eulerMascheroniConstant_eq_sum : Real.eulerMascheroniConstant = ∑' (n : ℕ), infiniteSumTerm n