lean_workbook_plus_61470

Proved

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

$a(2a^2-1)=0$ and so $a\in\left\{-\frac{\sqrt 2}2,0,+\frac{\sqrt 2}2\right\}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_61470 (a : ℝ) (h : a * (2 * a ^ 2 - 1) = 0) : a ∈ ({-Real.sqrt 2 / 2, 0, Real.sqrt 2 / 2} : Finset ℝ)   :=  by sorry

Source