lean_workbook_plus_2745
Provedwhich is obviously true by Muirhead
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2745 (x y z : ℝ) : x^6 + y^6 + z^6 ≥ x^4*y*z + y^4*z*x + z^4*x*y := by sorry
Source
which is obviously true by Muirhead
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_2745 (x y z : ℝ) : x^6 + y^6 + z^6 ≥ x^4*y*z + y^4*z*x + z^4*x*y := by sorry