lean_workbook_plus_72451
ProvedWe have :
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_72451 (a : ℝ) (h₀ : a ≠ 2) : 1 / (2 - a) = a * (a - 1)^2 / (2 * (2 - a)) + 1 / 2 * (a^2 + 1) := by sorry
Source
We have :
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_72451 (a : ℝ) (h₀ : a ≠ 2) : 1 / (2 - a) = a * (a - 1)^2 / (2 * (2 - a)) + 1 / 2 * (a^2 + 1) := by sorry