lean_workbook_plus_43402

Proved

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

So the condition actually is the equality case of AM-GM. So all of its variables $\frac ab; \frac bc;\frac ca$ are equal. (and, equal to $1$ ).

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_43402  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c)
  (h₁ : a + b + c = 1)
  (h₂ : a / b = b / c)
  (h₃ : b / c = c / a) :
  a / b = 1 ∧ b / c = 1 ∧ c / a = 1   :=  by sorry

Source

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

View graph