lean_workbook_plus_1474
ProvedThe sum of two nonzero real numbers is times their product. What is the sum of the reciprocals of the two numbers?
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1474 (x y : ℝ) (hx : x ≠ 0) (hy : y ≠ 0) (hxy : x + y = 4 * x * y) : x⁻¹ + y⁻¹ = 4 := by sorry
Source