lean_workbook_plus_79500

Proved

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

$a,b,c,x,y,z >0$ . $ax+by+cz=xyz \Leftrightarrow \frac{a}{yz}+\frac{b}{xz}+\frac{c}{xy}=1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79500 (a b c x y z : ℝ) : a>0 ∧ b>0 ∧ c>0 ∧ x>0 ∧ y>0 ∧ z>0 → (a * x + b * y + c * z = x * y * z ↔ a / y / z + b / x / z + c / x / y = 1)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph