lean_workbook_plus_70711

Proved

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

Prove the identity: $\frac1{(4n - 3)(4n - 1)} = \frac12(\frac1{4n - 3} - \frac1{4n - 1})$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_70711 (n : ℕ) (hn : n ≠ 0) : (1 : ℝ) / ((4 * n - 3) * (4 * n - 1)) = 1 / 2 * (1 / (4 * n - 3) - 1 / (4 * n - 1))   :=  by sorry

Source

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

View graph