lean_workbook_plus_9574

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Discuss the convergence of the series based on the behavior of the absolute value of the terms: $|\frac{(-1)^{\frac{n(n+3)}{2}}}{n}|=\frac{1}{n}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9574 : ∀ n : ℕ, |(-1 : ℝ)^((n*(n+3))/2)/n| = 1/n   :=  by sorry

Source