lean_workbook_plus_71317
ProvedSolve the equation .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_71317 (n : ℤ) : n^2 + 3*n - 2 = 2*n ↔ n = 1 ∨ n = -2 := by sorry
Source
Solve the equation .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_71317 (n : ℤ) : n^2 + 3*n - 2 = 2*n ↔ n = 1 ∨ n = -2 := by sorry