lean_workbook_plus_1714

Proved

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

Find the remainder when $2^{2011} + 3^{2011}+4^{2011}+5^{2011}+6^{2011}+7^{2011}+8^{2011}+2011$ is divided by 9.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1714 : 2 ^ 2011 + 3 ^ 2011 + 4 ^ 2011 + 5 ^ 2011 + 6 ^ 2011 + 7 ^ 2011 + 8 ^ 2011 + 2011 ≡ 3 [ZMOD 9]   :=  by sorry

Source