lean_workbook_plus_18565

Proved

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

$5(z+\frac{1}{z})=26$ , so $5z+\frac{5}{z}=26$ , so $5z^2-26z+5=0$ so $(z-5)(5z-1) = 0$ or $z=\frac{1}{5}, 5$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18565  (z : ℂ)
  (h₀ : 5 * (z + 1 / z) = 26) :
  z = 1 / 5 ∨ z = 5   :=  by sorry

Source