lean_workbook_plus_58230

Proved

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

Assume that two real numbers $a$ and $b$ satisfy $a^2+ab+b^2=1$ and $t=ab-a^2-b^2$ . Find the range for the values of $t$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58230 (a b t : ℝ) (h₁ : a^2 + a * b + b^2 = 1) (h₂ : t = a * b - a^2 - b^2) : ∃ a b, a^2 + a * b + b^2 = 1 ∧ t = a * b - a^2 - b^2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph