lean_workbook_plus_77183

Proved

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

So $a^2=4 \mbox{ and then } a=\pm2$ ??

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_77183  (a : ℝ)
  (h₀ : a^2 = 4) :
  a = 2 ∨ a = -2   :=  by sorry

Source