lean_workbook_plus_5639
ProvedProve that is divisible by 3 when mod .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_5639 (n : ℤ) (h : n ≡ 0 [ZMOD 3]) : n ^ 7 - n ≡ 0 [ZMOD 3] := by sorry
Source
Prove that is divisible by 3 when mod .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_5639 (n : ℤ) (h : n ≡ 0 [ZMOD 3]) : n ^ 7 - n ≡ 0 [ZMOD 3] := by sorry