lean_workbook_plus_67437
ProvedProve that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_67437 (x y z: ℝ) : x ^ 2 * y ^ 4 + z ^ 2 * x ^ 4 ≥ 2 * x ^ 3 * y ^ 2 * z := by sorry
Source
Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_67437 (x y z: ℝ) : x ^ 2 * y ^ 4 + z ^ 2 * x ^ 4 ≥ 2 * x ^ 3 * y ^ 2 * z := by sorry