lean_workbook_plus_18267

Proved

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

And $\dfrac{1}{\dfrac{1}{a^3} - \dfrac{1}{b^3}} = \dfrac{1}{\dfrac{b^3 - a^3}{a^3b^3}} = \dfrac{a^3b^3}{b^3 - a^3}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18267  (a b : ℝ)
  (h₀ : a ≠ 0 ∧ b ≠ 0)
  (h₁ : a ≠ b) :
  1 / (1 / a^3 - 1 / b^3) = a^3 * b^3 / (b^3 - a^3)   :=  by sorry

Source

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

View graph