lean_workbook_plus_14025

Proved

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

the 2 numbers are uniquely determined for each $P$ , but the three numbers are not. They have to be the solutions to $x^3 - Sx^2 + yx - P$ , where, if the solutions are $a$ , $b$ , and $c$ , then $y = ab + ac + bc$ or equivalently $-\frac{y}{P} = \frac{1}{a} + \frac{1}{b} + \frac{1}{c}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14025  (a b c p : ℂ)
  (f : ℂ → ℂ)
  (h₀ : ∀ x, f x = x^3 - p * x^2 + (a * b + a * c + b * c) * x - p)
  (h₁ : f a = 0)
  (h₂ : f b = 0)
  (h₃ : f c = 0)
  (h₄ : a ≠ b)
  (h₅ : a ≠ c)
  (h₆ : b ≠ c) :
  ∃ S y, ∀ x, f x = x^3 - S * x^2 + y * x - p   :=  by sorry

Source

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

View graph