lean_workbook_plus_59417

Proved

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

It is given that one root of $2x^2 + rx + s = 0$ , with $r$ and $s$ real numbers, is $3 + 2i (i = \sqrt { - 1})$ . The value of $s$ is: \n\n $\textbf{(A)}\ \text{undetermined} \qquad \textbf{(B)}\ 5 \qquad \textbf{(C)}\ 6 \qquad \textbf{(D)}\ - 13 \qquad \textbf{(E)}\ 26$ \n\nSince the coefficients of the quadratic are real, the other root is $3-2i$ and the product of the roots is $\frac{s}{2}=(3+2i)(3-2i)=9+4=13$ . \n\n $s=26$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_59417  (r s : ℝ)
  (f : ℂ → ℂ)
  (h₀ : ∀ z, f z = 2 * z^2 + r * z + s)
  (h₁ : f (3 + 2 * Complex.I) = 0) :
  s = 26   :=  by sorry

Source

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

View graph