Prove2Me

lean_workbook_plus_79539

Proved

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

proofwiki

Factor the series and split into two separate series.\n\nWe have n3−1n3+1\frac{n^3-1}{n^3+1} = (n−1)(n2+n+1)(n+1)(n2−n+1)\frac{(n-1)(n^2+n+1)}{(n+1)(n^2-n+1)} = n−1n+1n2+n+1n2−n+1\frac{n-1}{n+1} \frac{n^2+n+1}{n^2-n+1}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_79539 (n : ℕ) : ((n:ℝ)^3 - 1) / ((n:ℝ)^3 + 1) = (n - 1) / (n + 1) * ((n:ℝ)^2 + n + 1) / ((n:ℝ)^2 - n + 1)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph