lean_workbook_plus_42805
ProvedShow that , where and are real numbers.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_42805 (x y : ℝ) : (1 + x + y) ^ 2 ≥ 3 * (x + y + x * y) := by sorry
Source
Show that , where and are real numbers.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_42805 (x y : ℝ) : (1 + x + y) ^ 2 ≥ 3 * (x + y + x * y) := by sorry