lean_workbook_plus_68160

Proved

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

Find a quadratic equation with solutions $y1 = x1 + \frac{1}{x2}$ and $y2 = x2 + \frac{1}{x1}$ , given that $x1$ and $x2$ are solutions to the equation $3x^2 + 5x - 6 = 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68160 (x1 x2 y1 y2 : ℂ) (hx1 : 3 * x1 ^ 2 + 5 * x1 - 6 = 0) (hx2 : 3 * x2 ^ 2 + 5 * x2 - 6 = 0) (hy1 : y1 = x1 + 1 / x2) (hy2 : y2 = x2 + 1 / x1) : ∃ a b c : ℂ, a * y1 ^ 2 + b * y1 + c = 0 ∧ a * y2 ^ 2 + b * y2 + c = 0 ∧ a = 1 ∧ b = -(y1 + y2) ∧ c = y1 * y2   :=  by sorry

Source

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

View graph