Prove2Me

lean_workbook_plus_70465

Proved

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

Show that 7100≡1(mod100)7^{100} \equiv 1 \pmod{100} using the fact that 74≡1(mod100)7^4 \equiv 1 \pmod{100}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70465 : 7 ^ 100 ≡ 1 [ZMOD 100]   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph