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