lean_workbook_plus_39477
ProvedLet be reals such that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_39477 (x y : ℝ) : x^2 - 4 * x * y - y^2 ≤ 2 * x^2 + 3 * y^2 := by sorry
Source
Let be reals such that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_39477 (x y : ℝ) : x^2 - 4 * x * y - y^2 ≤ 2 * x^2 + 3 * y^2 := by sorry