lean_workbook_plus_3305
ProvedDerive the congruence .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3305 : ∀ k : ℕ, 2 ^ (3 * k) ≡ 1 [ZMOD 7] := by sorry
Source
Derive the congruence .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_3305 : ∀ k : ℕ, 2 ^ (3 * k) ≡ 1 [ZMOD 7] := by sorry