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