lean_workbook_plus_12430
ProvedThe product of two positive numbers is . The reciprocal of one of these numbers is times the reciprocal of the other number. What is the sum of the two numbers?
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12430 (x y : ℝ) (hx : x > 0 ∧ y > 0 ∧ x * y = 9) (h : 1/x = 4 * 1/y) : x + y = 15/2 := by sorry
Source