lean_workbook_plus_77493
ProvedProve:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_77493 : ∀ m n p : ℝ, (m + n + p) ^ 2 ≥ 3 * (m * n + n * p + m * p) := by sorry
Source
Prove:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_77493 : ∀ m n p : ℝ, (m + n + p) ^ 2 ≥ 3 * (m * n + n * p + m * p) := by sorry