lean_workbook_plus_74328
Provedand so
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_74328 {f : ℕ → ℕ} (h : f 1 = f 1 ^ 2) : f 1 = 0 ∨ f 1 = 1 := by sorrySource
and so
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_74328 {f : ℕ → ℕ} (h : f 1 = f 1 ^ 2) : f 1 = 0 ∨ f 1 = 1 := by sorry