lean_workbook_plus_75233

Proved

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

Use the M. Lasku's inequality: \n $2(a^2-ab+b^2)(c^2-cd+d^2)\geq a^2c^2+b^2d^2.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75233 {a b c d : ℝ} : 2 * (a ^ 2 - a * b + b ^ 2) * (c ^ 2 - c * d + d ^ 2) ≥ a ^ 2 * c ^ 2 + b ^ 2 * d ^ 2   :=  by sorry

Source