lean_workbook_plus_9423
ProvedWe have .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_9423 (a b : ℝ) (h₀ : a ≠ 0 ∧ b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b) := by sorry
Source
We have .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_9423 (a b : ℝ) (h₀ : a ≠ 0 ∧ b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b) := by sorry