lean_workbook_plus_40703

Proved

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

Let $z=\frac{3}{4},\quad y=\frac{4}{5},\quad x=\frac{5}{6}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_40703 (x y z : ℚ) (hx : x = 5 / 6) (hy : y = 4 / 5) (hz : z = 3 / 4) : x * y * z = 1 / 2   :=  by sorry

Source