lean_workbook_plus_36773

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

We know $2^{10}\equiv1\bmod 11$ so $2^{10n}\equiv1\bmod 11$ for any positive integer $n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_36773 (n : ℕ) : 2 ^ (10 * n) ≡ 1 [ZMOD 11]   :=  by sorry

Source