lean_workbook_plus_23556
ProvedProve that is congruent to 1 (mod 111).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_23556 : ∀ k : ℕ, 10 ^ (3 * k) ≡ 1 [ZMOD 111] := by sorry
Source
Prove that is congruent to 1 (mod 111).
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_23556 : ∀ k : ℕ, 10 ^ (3 * k) ≡ 1 [ZMOD 111] := by sorry