Prove2Me

lean_workbook_plus_33863

Proved

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

The other factor yields n2+5n+7=1 implies(n+2)(n+3)=0  ⟹  n=−2,n=−3 n^2+5n+7=1\ implies (n+2)(n+3)=0 \implies n=-2, n=-3

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_33863 {n : ℤ} (hn : n^2 + 5*n + 7 = 1) : n = -2 ∨ n = -3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph