lean_workbook_plus_70510

Proved

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

Given $x = 9/2$ and $y = 1/2$ , calculate $1/x + 1/y$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_70510 (x y : ℚ) (hx : x = 9/2) (hy : y = 1/2) : 1/x + 1/y = 20/9   :=  by sorry

Source