lean_workbook_plus_29093

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that $x^2-xy+y^2\leq \frac{3}{2}(x^2+y^2)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29093 : ∀ x y : ℝ, x ^ 2 - x * y + y ^ 2 ≤ (3 / 2) * (x ^ 2 + y ^ 2)   :=  by sorry

Source