lean_workbook_plus_21093Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)⟺(a+b+c)2≥3(ab+bc+ca)⟺2(a+b+c)2a2+b2+c2≥6(ab+bc+ca)a2+b2+c2\Longleftrightarrow (a+b+c)^2\ge 3(ab+bc+ca)\Longleftrightarrow \frac{2(a+b+c)^2}{a^2 + b^2 + c^2}\ge\frac{6(ab+bc+ca)}{a^2 + b^2 + c^2}⟺(a+b+c)2≥3(ab+bc+ca)⟺a2+b2+c22(a+b+c)2≥a2+b2+c26(ab+bc+ca)Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_21093 (a b c : ℝ) : (a + b + c) ^ 2 ≥ 3 * (a * b + b * c + c * a) ↔ 2 * (a + b + c) ^ 2 / (a ^ 2 + b ^ 2 + c ^ 2) ≥ 6 * (a * b + b * c + c * a) / (a ^ 2 + b ^ 2 + c ^ 2) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph