lean_workbook_plus_35325
ProvedProve that if is a factor of , then cannot be 1.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_35325 (n : ℕ) : n^2 - 1 ∣ 2010 → n ≠ 1 := by sorry
Source
Prove that if is a factor of , then cannot be 1.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_35325 (n : ℕ) : n^2 - 1 ∣ 2010 → n ≠ 1 := by sorry