lean_workbook_plus_43346

Proved

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

$\frac{1}{k^2-1} = \frac{1}{2} \left ( \frac{1}{k-1} - \frac{1}{k+1} \right ) \neq \frac {1}{k - 1} - \frac {1}{k}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_43346  (k : ℂ)
  (h₀ : k ≠ 1)
  (h₁ : k ≠ -1) :
  1 / (k^2 - 1) = 1 / 2 * (1 / (k - 1) - 1 / (k + 1))   :=  by sorry

Source