lean_workbook_plus_58533
ProvedIf holds for ALL integers, then
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_58533 (p : ℤ → ℤ) (h : ∀ x y : ℤ, x * p x = y * p y) : p 1 = 0 := by sorry
Source
If holds for ALL integers, then
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_58533 (p : ℤ → ℤ) (h : ∀ x y : ℤ, x * p x = y * p y) : p 1 = 0 := by sorry