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