Prove2Me

lean_workbook_plus_12936

Open

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

Prove that 2ϕ(77)≡260≡1 (mod 77)2^{\phi (77)} \equiv 2^{60} \equiv 1 \ (\text{mod } 77)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12936 : 2 ^ (Nat.totient 77) ≡ 1 [ZMOD 77]   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph