lean_workbook_plus_68898
Provedand so
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_68898 (f : ℤ → ℤ) (h : f (-1) = f (-1) ^ 2) : f (-1) = 0 ∨ f (-1) = 1 := by sorry
Source
and so
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_68898 (f : ℤ → ℤ) (h : f (-1) = f (-1) ^ 2) : f (-1) = 0 ∨ f (-1) = 1 := by sorry