lean_workbook_plus_4901

Proved

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

Consider the quadratic $x^2 - (4m + 1)x + 4m^2.$ If its roots are $r$ and $s,$ then $r + s = 4m + 1$ and $rs = 4m^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4901  (m r s : ℂ)
  (f : ℂ → ℂ)
  (h₀ : ∀ x, f x = x^2 - (4 * m + 1) * x + 4 * m^2)
  (h₁ : f r = 0)
  (h₂ : f s = 0)
  (h₃ : r ≠ s) :
  r + s = 4 * m + 1 ∧ r * s = 4 * m^2   :=  by sorry

Source

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

View graph