lean_workbook_plus_24456

Proved

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

Prove that $\frac{n^{2}}{n^{2}-1}=1+\frac{\frac{1}{2}}{n-1}-\frac{\frac{1}{2}}{n+1}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24456  (n : ℝ)
  (h₀ : n ≠ 1)
  (h₁ : n ≠ -1) :
  n^2 / (n^2 - 1) = 1 + 1 / (2 * (n - 1)) - 1 / (2 * (n + 1))   :=  by sorry

Source

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

View graph