lean_workbook_plus_35381
ProvedProve that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_35381 (a b c : ℝ) : a^2 + b^2 + c^2 - a * b - b * c - c * a ≥ 3 * (a - b) * (b - c) := by sorry
Source
Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_35381 (a b c : ℝ) : a^2 + b^2 + c^2 - a * b - b * c - c * a ≥ 3 * (a - b) * (b - c) := by sorry