lean_workbook_plus_14003

Proved

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

Now $a>2$ . We can transform equation $x^2+axy+y^2 = 1$ into $(x+a\frac{y}{2})^2 - (a^2 - 4)(\frac{y}{2})^2 = 1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14003 (a : ℝ) (ha : a > 2) (x y : ℝ) :  x^2 + a * x * y + y^2 = 1 ↔ (x + a * y / 2)^2 - (a^2 - 4) * (y / 2)^2 = 1   :=  by sorry

Source

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

View graph