lean_workbook_plus_15642

Proved

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

Simplest Vieta ..... $|\frac {(-1)^5.(18)}{2} - \frac {(-1)^2.(0)}{2}|=9$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_15642  (q e : ℝ)
  (h₀ : q = 18)
  (h₁ : e = 0) :
  abs ((-1)^5 * (q / 2) - (-1)^2 * (e / 2)) = 9   :=  by sorry

Source