lean_workbook_plus_25346
DisprovedProve that \n\n
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_25346 : ∀ a b : ℝ, a * b * (a ^ 4 + b ^ 4) + 2 * a * b ≥ 2 * a * b * (a ^ 2 + b ^ 2) := by sorry
Source
Prove that \n\n
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_25346 : ∀ a b : ℝ, a * b * (a ^ 4 + b ^ 4) + 2 * a * b ≥ 2 * a * b * (a ^ 2 + b ^ 2) := by sorry