lean_workbook_plus_58071
ProvedProve using Fermat's Little Theorem.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_58071 : 2 ^ (2017 - 1) ≡ 1 [ZMOD 2017] := by sorry
Source
Prove using Fermat's Little Theorem.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_58071 : 2 ^ (2017 - 1) ≡ 1 [ZMOD 2017] := by sorry