lean_workbook_plus_58045

Proved

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

From the sum, $\frac{a}r+a+ar = 5 \implies a\left(\frac{1}r+r+1\right) = 5$ $(1)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58045 (a r : ℝ) : a / r + a + a * r = 5 → a * (1 / r + r + 1) = 5   :=  by sorry

Source