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