lean_workbook_plus_74830
ProvedProve that for any integer .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_74830 (a : ℤ) : a^7 ≡ a [ZMOD 7] := by sorry
Source
Prove that for any integer .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_74830 (a : ℤ) : a^7 ≡ a [ZMOD 7] := by sorry