lean_workbook_plus_50112
ProvedIf and are distinct integers, using the binomial theorem, prove that is a factor of , whenever \n is a positive integer.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_50112 (a b : ℤ) (n : ℕ) : a - b ∣ a ^ n - b ^ n := by sorry
Source