lean_workbook_plus_75246

Proved

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

Explain why $|y| > |2y^2|$ when $-\frac{1}{2} < y < 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75246 (y : ℝ) (hy : -1 / 2 < y ∧ y < 0) : |y| > |2*y^2|   :=  by sorry

Source