lean_workbook_plus_31750
Provedand so or
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_31750 (a : ℝ) (f : ℝ → ℝ) (hf: (a-1)*f (-1) = 0) : f (-1) = 0 ∨ a = 1 := by sorry
Source
and so or
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_31750 (a : ℝ) (f : ℝ → ℝ) (hf: (a-1)*f (-1) = 0) : f (-1) = 0 ∨ a = 1 := by sorry