lean_workbook_plus_20759
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_20759 (a b c : ℝ) :
(a / b) ^ 2 + (b / c) ^ 2 + (c / a) ^ 2 ≥
1 / 3 * (a / b + b / c + c / a) ^ 2 := by sorrySource
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_20759 (a b c : ℝ) :
(a / b) ^ 2 + (b / c) ^ 2 + (c / a) ^ 2 ≥
1 / 3 * (a / b + b / c + c / a) ^ 2 := by sorry