lean_workbook_plus_18573
ProvedBy the Rearrangement Inequality,
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_18573 {p q r : ℝ} : p * q + q * r + r * p ≤ p ^ 2 + q ^ 2 + r ^ 2 := by sorrySource
By the Rearrangement Inequality,
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_18573 {p q r : ℝ} : p * q + q * r + r * p ≤ p ^ 2 + q ^ 2 + r ^ 2 := by sorry