lean_workbook_plus_1718
ProvedNow, .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1718 (r m o : ℝ) : (r + m + o) ^ 2 ≥ 3 * (r * m + m * o + o * r) := by sorry
Source
Now, .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_1718 (r m o : ℝ) : (r + m + o) ^ 2 ≥ 3 * (r * m + m * o + o * r) := by sorry