lean_workbook_plus_72940
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_72940 (D n: ℤ) (hn: D = -3 * n^2 + 6 * n + 1) (hD: D >= 0): n = 0 ∨ n = 1 ∨ n = 2 := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_72940 (D n: ℤ) (hn: D = -3 * n^2 + 6 * n + 1) (hD: D >= 0): n = 0 ∨ n = 1 ∨ n = 2 := by sorry