lean_workbook_plus_27087

Proved

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

For example, $\frac1{(n-1)n(n+1)}=(1/2)\frac1{n-1} + (-1)\frac1n+(1/2)\frac1{n+1}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_27087 (n : ℕ) (hn : 1 < n) : (1 : ℝ) / ((n - 1) * n * (n + 1)) = 1 / 2 * (1 / (n - 1)) - 1 * (1 / n) + 1 / 2 * (1 / (n + 1))   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph