lean_workbook_plus_48452

Proved

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

By Viete's Theorem again, $pq + qr + rp = 3c$ , $pqr =d$ .\n\n $p+r = 2q \Rightarrow pq + qr = 2q^2 \Rightarrow 3c - rp = 2q^2 \Rightarrow 3qc - pqr = 2q^3$ \n\nThus,\n\n $3bc - d = 2b^3$ \n\n $3bc - 2b^3 = d$ \nFurthermore, $c = \frac{d + 2b^3}{3b}, b \neq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_48452  (b c d : ℂ)
  (h₀ : b ≠ 0)
  (h₁ : 3 * b * c - 2 * b^3 = d) :
  c = (d + 2 * b^3) / (3 * b)   :=  by sorry

Source

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

View graph